From d858606e8400e6aab627f4aac5ec33ce9c2c80fe Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 20 May 2021 18:34:46 +0200 Subject: defines fsem (aka functional semantics) of BTL --- scheduling/RTLtoBTLproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 633e1b8e..60edea49 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -492,7 +492,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) E0 s2' + (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) E0 s2' /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) s2') \/ (omeasure oib' < n /\ E0=E0 /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)). @@ -523,7 +523,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. inversion MSTRONG; subst. inv MIB. @@ -677,7 +677,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. -- cgit From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 10:40:54 +0200 Subject: most of the proof BTL.fsem -> BTL.cfgsem. --- scheduling/RTLtoBTLproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 60edea49..feaac26f 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -727,9 +727,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. -- cgit