diff options
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 93f83450..4d785c10 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -260,6 +260,255 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. + +(*TODO Is this lemma too hard to read? *) + +Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: + forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1) + k ofin2 rs2 m2 + (CONT: match ofin1 with + | None => + (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) + \/ (exists rem, k = Some rem + /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2) + | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 + end), + iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2. +Proof. + induction 1; simpl. + { (* BF *) + destruct k; + intros ? ? ? (HRS & HM & HOF); subst. + eapply exec_seq_stop. all: constructor. } + (*destruct k; intros. try inv CONT.*) + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; + subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail); + inversion HR; subst; clear HR; + eapply exec_seq_continue; [ econstructor; eauto | assumption]. + - (* Bseq_stop *) + destruct k; intros; apply IHISTEP; eauto. + - (* Bseq_continue *) + destruct ofin; intros. + + destruct CONT as [HRS [HM HOF]]; subst. + eapply IHISTEP1; right. eexists; repeat split; eauto. + + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst. + * eapply IHISTEP1; right. eexists; repeat split; eauto. + eapply IHISTEP2; left; simpl; auto. + * eapply IHISTEP1; right. eexists; repeat split; eauto. + - (* Bcond *) + destruct ofin; intros; + econstructor; eauto; + destruct b; eapply IHISTEP; eauto. +Qed. + +(* TODO old version +Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin: + forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin) + k fin2 rs2 m2 + (CONT: match ofin with + | None => + exists rem, k = Some rem + /\ iblock_istep tge sp rs1 m1 rem rs2 m2 (Some fin2) + | Some fin => rs2=rs1 /\ m2=m1 /\ fin2=fin + end), + iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 (Some fin2). +Proof. + induction 1; simpl. + { (* BF *) + destruct k; + intros ? ? ? (HRS & HM & HOF); subst. + eapply exec_seq_stop. all: constructor. } + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct k; intros ? ? ? (rem & EQR & ISTEP); + inversion EQR; subst; clear EQR; + eapply exec_seq_continue; [ econstructor; eauto | assumption]. + - (* Bseq_stop *) + destruct k; intros; apply IHISTEP; eauto. + - (* Bseq_continue *) + destruct ofin; intros; apply IHISTEP1; + eexists; split; eauto. + - (* Bcond *) + destruct ofin; intros; + econstructor; eauto; + destruct b; eapply IHISTEP; auto. + Qed.*) + +Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: + iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> + iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin. +Proof. + intros; eapply expand_iblock_istep_rec_correct; eauto. + destruct ofin; simpl; auto. +Qed. + +(* TODO Which approach should we use here? *) +Lemma expand_iblock_istep_exact sp: + forall ib ofin rs0 m0 rs1 m1 + (ISTEP: iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin), + iblock_istep tge sp rs0 m0 ib rs1 m1 ofin. +Proof. Admitted. (* + induction ib; intros; + try (inv ISTEP; econstructor; eauto; fail). + - + rewrite iblock_istep_run_equiv in *. + inv ISTEP. simpl. + + + + destruct (iblock_istep_run tge sp (Bseq ib1 ib2) rs0 m0) eqn:?. + * destruct o. symmetry. + inv Heqo. + destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:?; try discriminate. + destruct o, _fin0 eqn:?; simpl in *. + rewrite <- iblock_istep_run_equiv in *. + eapply expand_iblock_istep_rec_correct; eauto. + inv Heqo0. simpl; auto. + rewrite H1. + rewrite <- iblock_istep_run_equiv in *. + eapply expand_iblock_istep_rec_correct; eauto. + simpl; right; eexists; split. eauto. + apply expand_iblock_istep_correct; auto. + * simpl in *. + destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:?; try discriminate. + destruct o; simpl in *. + destruct _fin eqn:?; simpl in *; try discriminate. + inv Heqo. + + inv ISTEP. simpl; repeat autodestruct; intros. + + destruct o; simpl in *. symmetry. + rewrite <- iblock_istep_run_equiv in *. + eapply expand_iblock_istep_rec_correct; eauto. + inv EQ. simpl; auto. + + destruct o; simpl in *. + rewrite H0. + rewrite <- iblock_istep_run_equiv in *. + destruct (iblock_istep_run tge sp ib2 _rs _m) eqn:?. + * eapply IHib2. destruct o. + rewrite <- iblock_istep_run_equiv in Heqo. + eapply expand_iblock_istep_rec_correct; eauto. + * destruct o; simpl in *. symmetry. + rewrite <- iblock_istep_run_equiv in *. + eapply expand_iblock_istep_rec_correct; eauto. + inv EQ; right. eexists; split. eauto. + apply expand_iblock_istep_correct; auto. + * destruct H0. + 2: { + rewrite iblock_istep_run_equiv in *. inv ISTEP. + destruct _fin eqn:?, o eqn:?; simpl in *. + 2:{ inv Heqo0. destruct ib1 + rewrite iblock_istep_run_equiv in *. inv ISTEP. + + - destruct ib1 eqn:?; simpl in *. + + rewrite iblock_istep_run_equiv in *. + simpl in *. auto. + + repeat econstructor. + rewrite iblock_istep_run_equiv in ISTEP. + simpl in *. + rewrite <- iblock_istep_run_equiv in ISTEP. + apply IHib2; auto. + + rewrite iblock_istep_run_equiv in ISTEP. + simpl in *. + destruct (eval_operation _ _ _ _) eqn:?; try discriminate. + repeat econstructor. eauto. simpl in *. + rewrite <- iblock_istep_run_equiv in ISTEP. + apply IHib2; auto. + + rewrite iblock_istep_run_equiv in ISTEP. + simpl in *. + destruct trap eqn:?; try discriminate. + destruct (eval_addressing _ _ _ _) eqn:?; try discriminate. + destruct (Mem.loadv _ _ _) eqn:?; try discriminate. + repeat econstructor; eauto. simpl in *. + rewrite <- iblock_istep_run_equiv in ISTEP. + apply IHib2; auto. + + rewrite iblock_istep_run_equiv in ISTEP. + simpl in *. + destruct (eval_addressing _ _ _ _) eqn:?; try discriminate. + destruct (Mem.storev _ _ _) eqn:?; try discriminate. + repeat econstructor; eauto. simpl in *. + rewrite <- iblock_istep_run_equiv in ISTEP. + apply IHib2; auto. + + destruct ofin. + * econstructor; eauto. simpl in *. + eapply IHib1; eauto. + + + + + eapply IHib1. + rewrite iblock_istep_run_equiv in *; simpl in *. + inv ISTEP. + destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1. + destruct _fin, o. inv ISTEP. + rewrite iblock_istep_run_equiv in *. + + destruct ib1; simpl in *. + + eapply IHib1. inv ISTEP.*) + +Lemma expand_preserves_iblock_istep_run sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = + iblock_istep_run tge sp (expand ib None) rs m. +Proof. Admitted. (* + intros. + destruct (iblock_istep_run tge sp (expand ib None) rs m) eqn:ISTEP. + (*destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.*) + - destruct o. + rewrite <- iblock_istep_run_equiv in *. + apply expand_iblock_istep_exact; auto. + - generalize dependent ib. + generalize dependent rs. + generalize dependent m. + induction ib; + try (intros; inv ISTEP; simpl; try autodestruct; fail). + + intros. inv ISTEP. simpl.*) + (* TODO Should we keep the None case in this lemma ? + destruct (iblock_istep_run tge sp ib1 rs m) eqn:EQib1; auto. + destruct o, _fin; simpl in *. + discriminate IHib1. + inv H0. + destruct IHib1. + rewrite <- iblock_istep_run_equiv in EQib1. + apply expand_iblock_istep_correct in EQib1. + discriminate IHib1. + apply EQib1 in IHib1. + inv EQib1. + 2: {, + destruct (iblock_istep_run tge sp (expand ib1 None) rs m) eqn:EQib1. + discriminate IHib1. + discriminate IHib1. + + + induction ib; try (simpl; auto; fail). + - intros. simpl. repeat autodestruct; intros. + + destruct o. symmetry. + rewrite <- iblock_istep_run_equiv in *. + simpl in EQ; rewrite EQ. + eapply expand_iblock_istep_rec_correct; eauto. + rewrite EQ; simpl; auto. + + destruct o. simpl in *. inv EQ. + rewrite <- iblock_istep_run_equiv in *. + 2: { intros. inv EQ. + - simpl.*) + +(* TODO +Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst opc: + forall (MIB: match_iblock dupmap cfg isfst pc ib opc) + k fin2 + (CONT: match opc with + | None => + exists rem, k = Some rem + /\ match_iblock dupmap cfg isfst pc rem (Some fin2) + | Some fin => fin2=fin + end), + match_iblock dupmap cfg isfst pc (expand ib k) (Some fin2). +Proof. + induction 1; simpl. + { destruct k. + intros; subst. econstructor. econstructor. + eapply exec_seq_stop. all: constructor. } + + Qed.*) + (** * Match strong state property Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2). @@ -291,6 +540,7 @@ See explanations of opt_simu below. >> *) + Lemma match_strong_state_simu dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) E0 (RTL.State st f sp pcR2 rs2 m2)) |