diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:34:46 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:34:46 +0200 |
| commit | d858606e8400e6aab627f4aac5ec33ce9c2c80fe (patch) | |
| tree | bcf193357cdaf9ee6a09fe36a4c9a0cb042c617a /scheduling/RTLtoBTLproof.v | |
| parent | 8dc70c68f241e1397f2c65981202742fb0ff75a3 (diff) | |
| download | compcert-kvx-d858606e8400e6aab627f4aac5ec33ce9c2c80fe.tar.gz compcert-kvx-d858606e8400e6aab627f4aac5ec33ce9c2c80fe.zip | |
defines fsem (aka functional semantics) of BTL
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |