diff options
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 121 |
1 files changed, 53 insertions, 68 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index c9e272c0..03329651 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -18,10 +18,10 @@ Local Open Scope list_scope. (** * Auxilary notions on simulation tests *) -Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop := +Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) outframe (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop := forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) -> exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) - /\ istate_simu f dm is1 is2. + /\ istate_simu f dm outframe is1 is2. (* a kind of negation of sabort_local *) Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := @@ -36,7 +36,7 @@ Proof. intuition congruence. Qed. -Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) := +Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) outframe (ctx: simu_proof_context f) (se1 se2: sistate_exit) := (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) -> (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) = @@ -47,10 +47,10 @@ Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) -> exists is2, ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2) - /\ istate_simu f dm is1 is2. + /\ istate_simu f dm outframe is1 is2. -Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) := - list_forall2 (siexit_simu dm f ctx) lse1 lse2. +Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) outframe (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) := + list_forall2 (siexit_simu dm f outframe ctx) lse1 lse2. (** * Implementation of Data-structure use in Hash-consing *) @@ -318,9 +318,9 @@ Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := (** ** Specification of the simulation test on [hsistate_local]. It is motivated by [hsilocal_simu_spec_correct theorem] below *) -Definition hsilocal_simu_spec (oalive: option Regset.t) (hst1 hst2: hsistate_local) := +Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) := List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) - /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> PTree.get r hst2 = PTree.get r hst1) + /\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1) /\ hsi_smem hst1 = hsi_smem hst2. Definition seval_sval_partial ge sp rs0 m0 hsv := @@ -368,18 +368,14 @@ Proof. - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto. Qed. -Theorem hsilocal_simu_spec_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2: - hsilocal_simu_spec of hst1 hst2 -> +Theorem hsilocal_simu_spec_correct hst1 hst2 alive ge1 ge2 sp rs0 m0 rs m st1 st2: + hsilocal_simu_spec alive hst1 hst2 -> hsilocal_refines ge1 sp rs0 m0 hst1 st1 -> hsilocal_refines ge2 sp rs0 m0 hst2 st2 -> (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> ssem_local ge1 sp st1 rs0 m0 rs m -> - match of with - | None => ssem_local ge2 sp st2 rs0 m0 rs m - | Some alive => - let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2) - in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs' - end. + let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2) + in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'. Proof. intros CORE HREF1 HREF2 GFS SEML. refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto. @@ -394,9 +390,8 @@ Proof. rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite smem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. } - destruct of as [alive |]. - - constructor. - + constructor; [assumption | constructor; [assumption|]]. + constructor. + + constructor; [assumption | constructor; [assumption|]]. destruct HREF2 as (B & _ & A & _). (** B is used for the auto below. *) assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto. @@ -420,17 +415,6 @@ Proof. unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity. ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj. rewrite <- C; [|assumption]. rewrite HST2. reflexivity. - - constructor; [|constructor]. - + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. - + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). - destruct CORE as (_ & _ & MEMEQ3). - rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. - erewrite smem_eval_preserved; [| eapply GFS]. - rewrite MEMEQ1; auto. - + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). - destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj. - rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS]. - unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto. Qed. (** ** Specification of the simulation test on [hsistate_exit]. @@ -438,17 +422,17 @@ Qed. *) Definition hsiexit_simu_spec dm f (hse1 hse2: hsistate_exit) := (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path - /\ hsilocal_simu_spec (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2)) + /\ hsilocal_simu_spec path.(input_regs) (hsi_elocal hse1) (hsi_elocal hse2)) /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1) /\ hsi_cond hse1 = hsi_cond hse2 /\ hsi_scondargs hse1 = hsi_scondargs hse2. -Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, +Definition hsiexit_simu dm f outframe (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, hsiexit_refines_stat hse1 se1 -> hsiexit_refines_stat hse2 se2 -> hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> - siexit_simu dm f ctx se1 se2. + siexit_simu dm f outframe ctx se1 se2. Lemma hsiexit_simu_spec_nofail dm f hse1 hse2 ge1 ge2 sp rs m: hsiexit_simu_spec dm f hse1 hse2 -> @@ -461,9 +445,9 @@ Proof. eapply hsilocal_simu_spec_nofail; eauto. Qed. -Theorem hsiexit_simu_spec_correct dm f hse1 hse2 ctx: +Theorem hsiexit_simu_spec_correct dm f outframe hse1 hse2 ctx: hsiexit_simu_spec dm f hse1 hse2 -> - hsiexit_simu dm f ctx hse1 hse2. + hsiexit_simu dm f outframe ctx hse1 hse2. Proof. intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2. assert (SEVALC: @@ -498,13 +482,13 @@ Proof. constructor; [|constructor]; simpl; auto. Qed. -Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2: - hsiexit_simu dm f ctx hse1 hse2 -> +Remark hsiexit_simu_siexit dm f outframe ctx hse1 hse2 se1 se2: + hsiexit_simu dm f outframe ctx hse1 hse2 -> hsiexit_refines_stat hse1 se1 -> hsiexit_refines_stat hse2 se2 -> hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> - siexit_simu dm f ctx se1 se2. + siexit_simu dm f outframe ctx se1 se2. Proof. auto. Qed. @@ -513,15 +497,15 @@ Qed. It is motivated by [hsiexit_simu_spec_correct theorem] below *) -Definition hsiexits_simu dm f (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop := - list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2. +Definition hsiexits_simu dm f outframe (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop := + list_forall2 (hsiexit_simu dm f outframe ctx) lhse1 lhse2. Definition hsiexits_simu_spec dm f lhse1 lhse2: Prop := list_forall2 (hsiexit_simu_spec dm f) lhse1 lhse2. -Theorem hsiexits_simu_spec_correct dm f lhse1 lhse2 ctx: +Theorem hsiexits_simu_spec_correct dm f outframe lhse1 lhse2 ctx: hsiexits_simu_spec dm f lhse1 lhse2 -> - hsiexits_simu dm f ctx lhse1 lhse2. + hsiexits_simu dm f outframe ctx lhse1 lhse2. Proof. induction 1; [constructor|]. constructor; [|apply IHlist_forall2; assumption]. @@ -529,8 +513,8 @@ Proof. Qed. -Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2, - siexits_simu dm f lse1 lse2 ctx -> +Lemma siexits_simu_all_fallthrough dm f outframe ctx: forall lse1 lse2, + siexits_simu dm f outframe lse1 lse2 ctx -> all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) -> (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx). @@ -545,8 +529,8 @@ Proof. Qed. -Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2: - siexits_simu dm f lse1 lse2 ctx -> +Lemma siexits_simu_all_fallthrough_upto dm f outframe ctx lse1 lse2: + siexits_simu dm f outframe lse1 lse2 ctx -> forall ext1 lx1, (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) -> @@ -570,14 +554,14 @@ Proof. Qed. -Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2: - hsiexits_simu dm f ctx lhse1 lhse2 -> +Lemma hsiexits_simu_siexits dm f outframe ctx lhse1 lhse2: + hsiexits_simu dm f outframe ctx lhse1 lhse2 -> forall lse1 lse2, hsiexits_refines_stat lhse1 lse1 -> hsiexits_refines_stat lhse2 lse2 -> hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 -> hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 -> - siexits_simu dm f lse1 lse2 ctx. + siexits_simu dm f outframe lse1 lse2 ctx. Proof. induction 1. - intros. inv H. inv H0. constructor. @@ -591,16 +575,16 @@ Qed. It is motivated by [hsistate_simu_spec_correct theorem] below *) -Definition hsistate_simu_spec dm f (hse1 hse2: hsistate) := +Definition hsistate_simu_spec dm f outframe (hse1 hse2: hsistate) := list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2) - /\ hsilocal_simu_spec None (hsi_local hse1) (hsi_local hse2). + /\ hsilocal_simu_spec outframe (hsi_local hse1) (hsi_local hse2). -Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, +Definition hsistate_simu dm f outframe (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, hsistate_refines_stat hst1 st1 -> hsistate_refines_stat hst2 st2 -> hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 -> hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 -> - sistate_simu dm f st1 st2 ctx. + sistate_simu dm f outframe st1 st2 ctx. Lemma list_forall2_nth_error {A} (l1 l2: list A) P: list_forall2 P l1 l2 -> @@ -644,9 +628,9 @@ Proof. rewrite H0; auto. Qed. -Theorem hsistate_simu_spec_correct dm f hst1 hst2 ctx: - hsistate_simu_spec dm f hst1 hst2 -> - hsistate_simu dm f hst1 hst2 ctx. +Theorem hsistate_simu_spec_correct dm f outframe hst1 hst2 ctx: + hsistate_simu_spec dm f outframe hst1 hst2 -> + hsistate_simu dm f outframe hst1 hst2 ctx. Proof. intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI. destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). @@ -655,22 +639,23 @@ Proof. - destruct SEMI as (SSEML & PCEQ & ALLFU). exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2. exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor. - + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]]. + + unfold ssem_internal. simpl. rewrite ICONT. admit. + (* constructor; [assumption | constructor; [reflexivity |]]. eapply siexits_simu_all_fallthrough; eauto. * eapply hsiexits_simu_siexits; eauto. * eapply nested_sok_prop; eauto. - eapply ssem_local_sok; eauto. + eapply ssem_local_sok; eauto. *) + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]]. constructor. - destruct SEMI as (ext & lx & SSEME & ALLFU). - assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). + assert (SESIMU: siexits_simu dm f outframe (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). exploit siexits_simu_all_fallthrough_upto; eauto. * destruct ALLFU as (ITAIL & ALLF). exploit nested_sok_tail; eauto. intros NESTED2. inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML. eapply nested_sok_prop; eauto. * intros (ext2 & lx2 & ALLFU2 & LENEQ). - assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { + assert (EXTSIMU: siexit_simu dm f outframe ctx ext ext2). { eapply list_forall2_nth_error; eauto. - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. @@ -683,7 +668,7 @@ Proof. + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). exists path. repeat (constructor; auto). -Qed. +Admitted. (** ** Specification of the simulation test on [sfval]. @@ -858,18 +843,18 @@ Qed. It is motivated by [hsstate_simu_spec_correct theorem] below *) -Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := - hsistate_simu_spec dm f (hinternal hst1) (hinternal hst2) +Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) := + hsistate_simu_spec dm f outframe (hinternal hst1) (hinternal hst2) /\ hfinal_simu_spec dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2). -Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop := +Definition hsstate_simu dm f outframe (hst1 hst2: hsstate) ctx: Prop := forall st1 st2, hsstate_refines hst1 st1 -> - hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx. + hsstate_refines hst2 st2 -> sstate_simu dm f outframe st1 st2 ctx. -Theorem hsstate_simu_spec_correct dm f ctx hst1 hst2: - hsstate_simu_spec dm f hst1 hst2 -> - hsstate_simu dm f hst1 hst2 ctx. +Theorem hsstate_simu_spec_correct dm f outframe ctx hst1 hst2: + hsstate_simu_spec dm f outframe hst1 hst2 -> + hsstate_simu dm f outframe hst1 hst2 ctx. Proof. intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2). generalize SCORE. intro SIMU; eapply hsistate_simu_spec_correct in SIMU; eauto. |