Module PLF_PLFO

Require Import List.
Import ListNotations.
Require Import Relations.

Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.
Require Import PLO.
Import PLF.

Refinement between PLF and PLFO machines


We can remove the checkpointing non-determinism from PLF by introducing the checkpointing oracle.

The refinement lemma is at the end of this file, stating that forall trace t, PLF.sem t -> ∃ o t', PLFO.sem o t' ∧ ∃ b, subtrace_chk b t t'.

Subtrace relation


Converting an event from PLFO into an event of PLF.
Definition PLFevent (e: PLFOevent): PLF.event :=
  match e with
  | PL.LogS => PLF.LogS
  | PL.LogF => PLF.LogF
  | PL.Op op => PLF.Op op
  end.

Definition of the subtrace_chk relation, filtering out portions of trace ending with a checkpointing failure.
Inductive subtrace_chk : bool -> PLF.trace -> PLFO.trace -> Prop :=
| committed_chk_end : forall b t t',
    subtrace_chk b t t' ->
    subtrace_chk true (ChkptS :: t) t'
| committed_chk_cons : forall e t t',
    subtrace_chk true t t' ->
    subtrace_chk true (PLFevent e :: t) (e :: t')
| ignored_chk_nil : subtrace_chk false [] []
| ignored_chk_end : forall b t t',
    subtrace_chk b t t' ->
    subtrace_chk false (ChkptF :: t) t'
| ignored_chk_cons : forall e t t',
    subtrace_chk false t t' ->
    subtrace_chk false (PLFevent e :: t) t'.

Unicity property for the subtrace_chk relation
Lemma subtrace_chk_unique: forall b t t',
    subtrace_chk b t t' ->
    forall b' t'',
      subtrace_chk b' t t'' ->
      b' = b /\ t'' = t'.
Proof.
  induction 1; intros.

  - inv H0.
    + apply IHsubtrace_chk in H3; auto.
      intuition.
    + destruct e ; inv H1.
    + destruct e ; inv H1.

  - inv H0.
    + destruct e ; inv H1.
    + assert (e0 = e).
      { destruct e, e0 ; inv H1; auto. }
      subst.
      apply IHsubtrace_chk in H5; auto.
      intuition. congruence.
    + destruct e ; inv H1.
    + assert (e0 = e).
      { destruct e, e0 ; inv H1; auto. }
      subst.
      apply IHsubtrace_chk in H5; auto.
      intuition. inv H0.

  - inv H; auto.

  - inv H0.
    + destruct e ; inv H1.
    + apply IHsubtrace_chk in H3; auto.
      intuition.
    + destruct e ; inv H1.

  - inv H0; auto.
    
    + destruct e ; inv H1.
    + assert (e0 = e).
      { destruct e, e0 ; inv H1; auto. }
      subst.
      apply IHsubtrace_chk in H5; auto.
      intuition. inv H0.
    + destruct e ; inv H1.
Qed.

Lemma subtrace_chk_concat: forall b t t',
    subtrace_chk b t t' ->
    forall e,
      if b then subtrace_chk b (map PLFevent e ++ t) (e ++ t')
      else subtrace_chk b (map PLFevent e ++ t) t'.
Proof.
  induction e ; intros.
  - simpl. destruct b; auto.
  - destruct b.
    + simpl. econstructor; eauto.
    + simpl. econstructor; eauto.
Qed.

Lemma subtrace_chkpt_ops: forall op,
    subtrace_chk false (map PLFevent op) [].
Proof.
  induction op.
  - constructor.
  - simpl. econstructor; eauto.
Qed.

Alternative, equivalent definition of the subtrace relation subtrace_chk, easier to use in the proof of refinement.
Inductive subtrace_chk_alt : bool -> PLF.trace -> PLFO.trace -> Prop :=
| committed_chk_aend : forall b t t',
    subtrace_chk_alt b t t' ->
    subtrace_chk_alt true (ChkptS :: t) t'
| committed_chk_acons : forall e t t',
    subtrace_chk_alt true t t' ->
    subtrace_chk_alt true ((map PLFevent e) ++ t) (e ++ t')
| ignored_chk_anil : subtrace_chk_alt false [] []
| ignored_chk_aend : forall b t t',
    subtrace_chk_alt b t t' ->
    subtrace_chk_alt false (ChkptF :: t) t'
| ignored_chk_acons : forall e t t',
    subtrace_chk_alt false t t' ->
    subtrace_chk_alt false ((map PLFevent e) ++ t) t'.

Lemma subtrace_chk_subtrace_chk_alt : forall b t t',
    subtrace_chk b t t' ->
    subtrace_chk_alt b t t'.
Proof.
  induction 1; intros; try solve [econstructor; eauto].
  - replace (PLFevent e :: t) with (map PLFevent (e::nil) ++ t) by auto with datatypes.
    replace (e:: t') with ([e] ++ t') by auto with datatypes.
    econstructor ; eauto.
  - replace (PLFevent e :: t) with (map PLFevent (e::nil) ++ t) by auto with datatypes.
    econstructor ; eauto.
Qed.
  
Lemma subtrace_chk_alt_subtrace_chk: forall b t t',
    subtrace_chk_alt b t t' ->
    subtrace_chk b t t'.
Proof.
  induction 1; intros; try solve [econstructor; eauto].
  - eapply subtrace_chk_concat in IHsubtrace_chk_alt; eauto.
  - eapply subtrace_chk_concat in IHsubtrace_chk_alt; eauto.
Qed.

Refinement proof


Converting a PLF state into a PLFO state by including the oracle.
Definition lift_chk (o : oracle)(s: PLF.state): PLFO.state :=
  match s with
  | INIT => PLFO.INIT o
  | USR x x0 x1 => PLFO.USR o x x0 x1
  | DRV x x0 x1 x2 => PLFO.DRV o x x0 x1 x2
  | PWR x => PLFO.PWR o x
  | OFF x => PLFO.OFF o x
  end.

Helper lemma to reason about the empty oracle -- the empty trace is produced.
Lemma empty_run: forall s t s',
    (exists s0, lift_chk [] s0 = s) ->
    run PLFO.step s t s' ->
    exists s'2, t = [] /\ lift_chk [] s'2 = s'.
Proof.
  intros.
  induction H0; intros; auto.
  - inv H0;
      destruct H as [s0 H3]; destruct s0; inv H3.
    + exists (USR MCU.init DEV.init CHKPT.init).
      try eexists; try split; simpl; eauto;
        try reflexivity.
    + exists (USR mcu' dev' chkpt).
      try eexists; try split; simpl; eauto;
        try reflexivity.
      assert (t0 = []) as -> by (eapply SPEC.axiom_usr ; eauto).
      auto.
    + exists (DRV mcu' dev' (CHKPT.next_log chkpt) (CHKPT.saveNextMCU chkpt mcu)).
      try eexists; try split; simpl; eauto;
        try reflexivity.
      assert (t0 = []) as -> by (eapply SPEC.axiom_enter ; eauto).
      auto.
    + exists (PWR (CHKPT.saveNextMCU chkpt mcu)).
      try eexists; try split; simpl; eauto;
        try reflexivity.
    + exists (USR (CHKPT.last_mcu chkpt) (LOG.restore (CHKPT.last_log chkpt))
                  (CHKPT.reset chkpt)).
      try eexists; try split; simpl; eauto;
        try reflexivity.
  - destruct H as [s Hs].
    eexists; eauto.
  - apply IHrun1 in H.
    destruct H as [s2 [-> Hs2]].
    simpl.
    eapply IHrun2.
    eauto.
Qed.

Helper lemma to exhibit the oracle generating the subtrace.
Lemma gen_checkpointing_oracle : forall si t sf,
    run_right PLF.step si t sf ->
    exists
      (o : oracle) (t' : PLFO.trace)
      (sf' : PLFO.state),
      run PLFO.step (lift_chk o si) t' sf'
      /\
      match o with
      | [] => subtrace_chk_alt false t t'
      | true :: _ => subtrace_chk_alt true t t'
      | false :: _ => subtrace_chk_alt false t t'
      end.
Proof.
  intros.
  induction H.
  - (* refl *)
    exists [].
    exists [].
    exists (lift_chk [] x).
    repeat split; try eapply run_refl; econstructor.
    
  - (* step *)
    enough (CASE x t1 y); [| constructor].
    destruct IHrun_right as [o [t' [sf' [Hrun Hsub]]]].
    destruct STEP.
    + (* INIT -> USR *)
      simpl.
      eexists o.
      eexists t'.
      eexists sf'.
      repeat split; auto.
      change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step; econstructor; eauto.

    + (* USR -> USR *)
      simpl.
      eexists o.
      eexists t'.
      eexists sf'.
      pose proof (SPEC.axiom_usr _ _ _ _ _ INSTR) as [-> ->].
      repeat split; auto.
      change t' with ([] ++ t').
      change [] with (map PL.Op []).
      eapply run_trans; eauto.
      eapply run_step; econstructor ; eauto.
      
    + (* USR -> DRV *)
      destruct o; [|destruct b].
      * (* ignoring *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.
      * (* committing *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.
      * (* ignoring *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.

    + (* DRV -> DRV *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [].
        eexists [].
        exists ((lift_chk []
                          (DRV mcu dev l chkpt))).
        repeat split.
        -- eapply run_refl.
        -- change (map Op t ++ t2) with
               (map (fun o => PLFevent (PL.Op o)) t ++ t2).
           rewrite <- map_map.
           apply ignored_chk_acons.
           apply empty_run in Hrun as [_ [-> _]];
             auto.
           eexists; eauto.
      * eexists (true :: o).
        eexists ((map PL.Op t) ++ t').
        eexists sf'.
        repeat split; eauto.
        -- simpl.
           eapply run_trans; eauto.
           eapply run_step.
           simpl.
           change (map PL.Op t) with (if true then (map PL.Op t) else []).
           eapply PLFO.sem_drv; eauto.
        -- change (map Op t ++ t2) with
               (map (fun o => PLFevent (PL.Op o)) t ++ t2).
           rewrite <- map_map.
           constructor. auto.
      * exists (false :: o).
        exists ([] ++ t').
        exists sf'.
        repeat split; eauto.
        ++ eapply run_trans; eauto.
           eapply run_step.
           simpl.
           change [] with (if false then (map PL.Op t) else []).
           eapply PLFO.sem_drv; eauto.
        ++ change (map Op t ++ t2) with
               (map (fun o => PLFevent (PL.Op o)) t ++ t2).
           rewrite <- map_map.
           econstructor; auto.
           
    + (* DRV -> USR *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [].
        eexists [].
        exists ((lift_chk []
                          (DRV mcu dev l chkpt))).
        repeat split.
        -- eapply run_refl.
        -- change [LogS] with (map PLFevent [PL.LogS]).
           rewrite <- app_assoc.
           change (map Op t) with (map (fun o => PLFevent (PL.Op o)) t).
           rewrite <- map_map.
           apply ignored_chk_acons.
           apply ignored_chk_acons.
           apply empty_run in Hrun as [_ [-> _]];
             auto.
           eexists; eauto.
           
      * eexists (true::o).
        eexists.
        eexists.
        pose proof (SPEC.axiom_leave _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        eapply PLFO.sem_leave; eauto.
        simpl.
        change (LogS :: t2) with ((map PLFevent [PL.LogS])++t2).
        change (PL.LogS :: t') with ([PL.LogS] ++ t').
        econstructor; eauto.

      * exists (false :: o).
        eexists.
        eexists.
        pose proof (SPEC.axiom_leave _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        
        ++ eapply run_trans; eauto.
           eapply run_step.
           eapply PLFO.sem_leave; eauto.
           
        ++ simpl.
           change (LogS :: t2) with ((map PLFevent [PL.LogS])++t2).
           econstructor; auto.

    + (* USR -> PWR *)
      eexists.
      eexists.
      eexists.
      repeat split; eauto.
      simpl. change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step.
      econstructor; eauto.
      
    + (* DRV -> PWR *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [].
        eexists [].
        exists ((lift_chk []
                          (DRV mcu dev l chkpt))).
        repeat split.
        -- eapply run_refl.
        -- change [LogF] with (map PLFevent [PL.LogF]).
          apply ignored_chk_acons.
          apply empty_run in Hrun as [_ [-> _]];
            auto.
          eexists; eauto.
          
      * eexists (true::o).
        eexists.
        eexists.
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        eapply PLFO.sem_pwr_drv; eauto.
        simpl.
        change (LogF :: t2) with ((map PLFevent [PL.LogF])++t2).
        change (PL.LogF :: t') with ([PL.LogF] ++ t').
        econstructor; eauto.

      * exists (false :: o).
        eexists.
        eexists.
        repeat split; eauto.
        ++ eapply run_trans; eauto.
           eapply run_step.
           econstructor; eauto.
        ++ simpl.
           change (LogF :: t2) with ((map PLFevent [PL.LogF])++t2).
           econstructor; auto.
           
    + (* PWR -> OFF with commit *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [true].
        eexists [].
        exists ((lift_chk [true] (PWR chkpt))).
        repeat split.
        -- eapply run_refl.
        -- simpl.
           econstructor ; eauto.
           eapply empty_run in Hrun as [_ [-> _]];
             eauto.
           
      * eexists (true::true::o).
        eexists ([]++t').
        eexists.
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. econstructor; eauto.

      * exists (true::false::o).
        eexists.
        eexists.
        repeat split.
        -- eapply run_trans.
           eapply run_step; eauto.
           eapply PLFO.sem_chkpt_success; eauto.
           eapply Hrun.
        -- simpl.
           econstructor; eauto.
           
    + (* PWR -> OFF without commit *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [].
        eexists [].
        exists ((lift_chk [] (PWR chkpt))).
        repeat split.
        -- eapply run_refl.
        -- simpl.
           econstructor; eauto.
           eapply empty_run in Hrun as [_ [-> _]];
             eauto.
           
      * exists (false::true::o).
        eexists.
        eexists.
        repeat split.
        -- eapply run_trans; eauto.
           eapply run_step; eauto.
           econstructor; eauto.
           
        -- simpl.
           econstructor; eauto.
        
      * eexists (false::false::o).
        eexists ([]++t').
        eexists.
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step; eauto.
        econstructor; eauto.
        econstructor; eauto.
        
    + (* OFF -> USR *)
      destruct o; [| destruct b].
      * eexists [].
        eexists [].
        eexists.
        repeat split; eauto.
        simpl. eapply run_refl; eauto.
        apply empty_run in Hrun as [_ [-> _]];
          auto.
        eexists; eauto.

      * exists (true::o).
        exists ([]++t').
        eexists sf'.
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step; eauto.
        econstructor; eauto.

      * exists (false::o).
        exists ([]++t').
        exists sf'.
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step; eauto.
        econstructor; eauto.

    + destruct o; [| destruct b].

      * eexists [].
        exists [].
        eexists.
        repeat split; eauto.
        simpl. eapply run_refl; eauto.
        simpl.
        eapply empty_run in Hrun as [_ [-> _]];
          eauto.
        econstructor; eauto.
        
      * exists (false::true::o).
        exists ([]++t').
        eexists.
        split.
        -- eapply run_trans.
           apply run_step.
           simpl.
           eapply PLFO.sem_usr_off; eauto.
           eapply Hrun.
        -- econstructor; eauto.

      * exists (false::false::o).
        exists ([]++t').
        eexists.
        split.
        -- eapply run_trans.
           apply run_step.
           simpl.
           eapply PLFO.sem_usr_off; eauto.
           eapply Hrun.
        -- econstructor; eauto.
           
    + destruct o; [| destruct b].

      * eexists [].
        exists [].
        eexists.
        repeat split; eauto.
        simpl. eapply run_refl; eauto.
        simpl.
        eapply empty_run in Hrun as [_ [-> _]];
          eauto.
        econstructor; eauto.

      * exists (false::true::o).
        exists ([]++t').
        eexists.
        split.
        -- eapply run_trans.
           apply run_step.
           simpl.
           eapply PLFO.sem_drv_off; eauto.
           eapply Hrun.
        -- econstructor; eauto.
           
      * exists (false::false::o).
        exists ([]++t').
        eexists.
        split.
        -- eapply run_trans.
           apply run_step.
           simpl.
           eapply PLFO.sem_drv_off; eauto.
           eapply Hrun.
        -- econstructor; eauto.
Qed.

Validity of checkpointing oracle.
Lemma checkpoint_validity : forall t,
    PLF.sem t ->
    exists o t', PLFO.sem o t' /\ exists b, subtrace_chk b t t'.
Proof.
  intros t [s Hsem].
  eapply run_run_right in Hsem.
  apply gen_checkpointing_oracle in Hsem as [o [t' [sf' [Hrun H]]]].
  exists o.
  exists t'.
  split.
  - econstructor.
    eauto.
  - destruct o; eauto using subtrace_chk_alt_subtrace_chk.
    destruct b; eauto using subtrace_chk_alt_subtrace_chk.
Qed.




Generated by coq2html