diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:00:51 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:00:51 +0200 |
| commit | ef5775ea869701eb04c873174c362b314166bf06 (patch) | |
| tree | 634c5364ec95dc649e302a63dee72eadb0e6b73b /scheduling/RTLtoBTLproof.v | |
| parent | 05b24fdb11414100b9b04867e6e2d3a1a9054162 (diff) | |
| parent | 43ab0b948ac379e55bbe334a0a541c1680437fbf (diff) | |
| download | compcert-kvx-ef5775ea869701eb04c873174c362b314166bf06.tar.gz compcert-kvx-ef5775ea869701eb04c873174c362b314166bf06.zip | |
Merge branch 'BTL_fsem' into BTL
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f561ee7a..7d83931b 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -538,7 +538,7 @@ Lemma match_strong_state_simu (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false) (MES : measure ib2 < n) : exists (oib' : option iblock), - (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' + (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) E0 s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < n /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). @@ -566,7 +566,7 @@ Lemma opt_simu_intro (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) (NGOTO : is_goto ib = false) : exists (oib' : option iblock), - (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') + (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). Proof. inv MSTRONG; subst. inv MIB. @@ -699,7 +699,7 @@ Theorem opt_simu s1 t s1' oib s2: RTL.step ge s1 t s1' -> match_states oib s1 s2 -> exists (oib' : option iblock), - (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2') + (exists s2', step tid tge s2 t s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) . Proof. @@ -738,9 +738,9 @@ Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (BTL.semantics tprog). + forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog). Proof. - eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). constructor 1; simpl. - apply well_founded_ltof. - eapply transf_initial_states. |