Module plf

Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.

LOG: Device operations logging


Module LOG.

Type of operation logs, and initial log.
  Parameter t : Type.
  Parameter init: t.

Add an operation to a log.
  Parameter log: t -> DEV.ops -> t.

Adding a list of operations to a log.
  Definition log_ops (l: LOG.t) (t: list DEV.ops) (l': LOG.t) :=
    fold_left LOG.log t l = l'.

Restoring a peripheral device state from a log.
  Parameter restore: t -> DEV.t.

Below are the required and derived properties of the operation logging.
  Axiom restore_init: DEV.equiv (restore init) DEV.init.

  Axiom restore_log: forall l dev dev' op,
      DEV.equiv (restore l) dev ->
      DEV.op_sem (projT1 op) dev (projT2 op) dev' ->
      DEV.equiv (restore (log l op)) dev'.

  Lemma restore_log_trace : forall t l dev dev',
      DEV.ops_sem t dev dev' ->
      DEV.equiv (restore l) dev ->
      DEV.equiv (restore (fold_left log t l)) dev'.
  Proof.
    induction t0 ; intros.
    - simpl. inv H. auto.
    - simpl. inv H.
      eapply IHt0; eauto using equiv_refl.
      eapply restore_log; eauto.
  Qed.
  
End LOG.

CHKPT: Non-volatile checkpointing storage


Module CHKPT.

Type definition for non-volatile checkpointing storage.
  Record t := CHKPT { last_mcu : MCU.t ; last_log : LOG.t ;
                      next_mcu : MCU.t ; next_log : LOG.t }.

Initial non-volatile checkpointing storage.
  Definition init: t := CHKPT MCU.init LOG.init
                              MCU.init LOG.init.


Committing the next snapshot as the last valid snapshot.
  Definition set (chkpt: t): t :=
    CHKPT chkpt.(next_mcu) chkpt.(next_log)
          chkpt.(next_mcu) chkpt.(next_log).

Discarding the next snapshot by resetting it to the last valid snapshot.
  Definition reset (chkpt: t): t :=
    CHKPT chkpt.(last_mcu) chkpt.(last_log)
          chkpt.(last_mcu) chkpt.(last_log).

Updating the next log.
  Definition saveNextLog (chkpt: t)(l: LOG.t): t :=
    CHKPT chkpt.(last_mcu) chkpt.(last_log)
          chkpt.(next_mcu) l.

Updating the next MCU snapshot.
  Definition saveNextMCU (chkpt: t)(mcu: MCU.t): t :=
    CHKPT chkpt.(last_mcu) chkpt.(last_log)
          mcu chkpt.(next_log).

End CHKPT.

PLF


Interrupt-based checkpointing model with failures. It is non-deterministic in
Module PLF.

PLF execution states.
  Inductive state :=
  | INIT : state (* initial state *)
  | USR : MCU.t -> DEV.t -> CHKPT.t -> state (* user-mode state *)
  | DRV : MCU.t -> DEV.t -> LOG.t -> CHKPT.t -> state (* driver mode *)
  | PWR : CHKPT.t -> state (* power-loss interrupt raised *)
  | OFF : CHKPT.t -> state. (* power ran out *)

PLF observable events.
  Inductive event :=
  | ChkptS: event (* checkpoint success *)
  | ChkptF: event (* checkpoint failure *)
  | LogS : event (* power-continuous section completed *)
  | LogF : event (* power-continuous section aborted *)
  | Op : DEV.ops -> event. (* device operation *)
  
  Definition trace := list event.

Transition relation.
  Inductive step : state -> trace -> state -> Prop :=
  | step_firstboot:
      step INIT
           []
           (USR MCU.init DEV.init CHKPT.init)

  | sem_usr: forall mcu mcu' dev dev' chkpt t,
      forall (INSTR: SPEC.step (SPEC.STATE SPEC.Usr mcu dev)
                               t
                               (SPEC.STATE SPEC.Usr mcu' dev')),
        step (USR mcu dev chkpt)
             (map Op t)
             (USR mcu' dev' chkpt)

  | sem_enter: forall mcu mcu' dev dev' chkpt chkpt' t l,
      forall (INSTR: SPEC.step (SPEC.STATE SPEC.Usr mcu dev)
                               t
                               (SPEC.STATE SPEC.Drv mcu' dev'))
             (RUNTIME1: CHKPT.saveNextMCU chkpt mcu = chkpt')
             (RUNTIME2: l = CHKPT.next_log chkpt),
        step (USR mcu dev chkpt)
             (map Op t)
             (DRV mcu' dev' l chkpt')

  | sem_drv: forall mcu mcu' dev dev' l l' chkpt t,
      forall (INSTR: SPEC.step (SPEC.STATE SPEC.Drv mcu dev)
                               t
                               (SPEC.STATE SPEC.Drv mcu' dev'))
             (RUNTIME: LOG.log_ops l t l'),
        step (DRV mcu dev l chkpt)
             (map Op t)
             (DRV mcu' dev' l' chkpt)

  | sem_leave: forall mcu mcu' dev dev' l chkpt chkpt' t,
      forall (INSTR: SPEC.step (SPEC.STATE SPEC.Drv mcu dev)
                               t
                               (SPEC.STATE SPEC.Usr mcu' dev'))
             (RUNTIME: CHKPT.saveNextLog chkpt l = chkpt'),
        step (DRV mcu dev l chkpt)
             (map Op t ++ [LogS])
             (USR mcu' dev' chkpt')

  | sem_pwr_usr: forall mcu dev chkpt chkpt',
      forall (RUNTIME: CHKPT.saveNextMCU chkpt mcu = chkpt'),
        step (USR mcu dev chkpt)
             []
             (PWR chkpt')

  | sem_pwr_drv: forall chkpt mcu dev l,
      step (DRV mcu dev l chkpt)
           [LogF]
           (PWR chkpt)

  | sem_chkpt_success: forall chkpt chkpt',
      forall (RUNTIME: CHKPT.set chkpt = chkpt'),
        step (PWR chkpt)
             [ChkptS]
             (OFF chkpt')

  | sem_chkpt_failure: forall chkpt,
      step (PWR chkpt)
           [ChkptF]
           (OFF chkpt)

  | sem_reboot: forall chkpt dev mcu chkpt',
      forall (RUNTIME1: mcu = CHKPT.last_mcu chkpt)
             (RUNTIME2: dev = LOG.restore (CHKPT.last_log chkpt))
             (RUNTIME3: chkpt' = CHKPT.reset chkpt),
        step (OFF chkpt)
             []
             (USR mcu dev chkpt')

  | sem_usr_off: forall mcu dev chkpt,
      step (USR mcu dev chkpt)
           [ChkptF]
           (OFF chkpt)
           
  | sem_drv_off: forall chkpt mcu dev l,
      step (DRV mcu dev l chkpt)
           [ChkptF]
           (OFF chkpt)
  .

Trace semantics.
  Definition sem (t: list event): Prop :=
    exists s, run step INIT t s.

End PLF.