From fddab2ea68a4770f14188d120a83d45894acfbda Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 10:01:02 +0200 Subject: cleaner match_states --- scheduling/RTLtoBTLproof.v | 37 +++++++++++++++++++++---------------- 1 file changed, 21 insertions(+), 16 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 4f76d0b7..2116ac70 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -83,11 +83,11 @@ Local Open Scope nat_scope. (* TODO: faire un dessin ASCII art de la simulation avec match_states_intro -Le iblock en paramètre représente l'état de l'exécution côté BTL +Le (option iblock) en paramètre représente l'état de l'exécution côté BTL depuis le début de l'exécution du block *) -Inductive match_states: iblock -> RTL.state -> state -> Prop := +Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *) ib dupmap st f sp pc rs m st' f' pc' pc0' pc0 rs0 m0 isfst ib0 (STACKS: list_forall2 match_stackframes st st') @@ -98,16 +98,16 @@ Inductive match_states: iblock -> RTL.state -> state -> Prop := (RIGHTA: is_right_assoc ib) (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m)) (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m) - : match_states ib (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m) + : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m) | match_states_call - ib st st' f f' args m + st st' f f' args m (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_fundef f f') - : match_states ib (RTL.Callstate st f args m) (Callstate st' f' args m) + : match_states None (RTL.Callstate st f args m) (Callstate st' f' args m) | match_states_return - ib st st' v m + st st' v m (STACKS: list_forall2 match_stackframes st st') - : match_states ib (RTL.Returnstate st v m) (Returnstate st' v m) + : match_states None (RTL.Returnstate st v m) (Returnstate st' v m) . Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -161,7 +161,7 @@ Proof. - constructor; eauto. constructor. apply transf_fundef_correct; auto. -Admitted. (* TODO *) +Qed. Lemma transf_final_states ib s1 s2 r: match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r. @@ -209,13 +209,18 @@ La hauteur de l'arbre aussi. *) Parameter measure: iblock -> nat. -Theorem opt_simu s1 t s1': +Definition omeasure (oib: option iblock): nat := + match oib with + | None => 0 + | Some ib => measure ib + end. + +Theorem opt_simu s1 t s1' oib s2: RTL.step ge s1 t s1' -> - forall ib s2, - match_states ib s1 s2 -> - exists (ib' : iblock), - (exists s2', step tge s2 t s2' /\ match_states ib' s1' s2') - \/ (measure ib' < measure ib /\ t=E0 /\ match_states ib' s1' s2) + match_states oib s1 s2 -> + exists (oib' : option iblock), + (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2') + \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) . Admitted. @@ -224,13 +229,13 @@ Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (BTL.semantics tprog). Proof. - eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ measure) match_states). + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). constructor 1; simpl. - apply well_founded_ltof. - eapply transf_initial_states. - eapply transf_final_states. - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP. - destruct 1 as (ib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]). + destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]). + repeat eexists; eauto. + subst. repeat eexists; eauto. - eapply senv_preserved. -- cgit