From 8999ea0a952381a4ba94b5266a268ec350bf3f2d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 12 May 2021 08:51:05 +0200 Subject: ascii simu --- scheduling/RTLtoBTLproof.v | 65 ++++++++++++++++++++++++++++++++++------------ 1 file changed, 48 insertions(+), 17 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 7d039f11..93f83450 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -91,18 +91,18 @@ The simulation diagram for match_states_intro is as follows: << RTL state match_states_intro BTL state - [pcR0,rs0,m0] ---------------------------- [pcB0,rs0,m0] + [pcR0,rs0,m0] --------------------------- [pcB0,rs0,m0] | | | | RTL_RUN | *E0 | BTL_RUN | | | MIB | - [pcR1,rs,m] -------------------------------- [ib] + [pcR1,rs1,m1] ------------------------------- [ib] >> *) -Inductive match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: Prop := +Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: Prop := | match_strong_state_intro (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') @@ -110,17 +110,17 @@ Inductive match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib (DUPLIC: dupmap!pcB0 = Some pcR0) (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) (IS_EXPD: is_expand ib) - (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m)) - (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m) - : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst + (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs1 m1)) + (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs1 m1) + : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst . Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := | match_states_intro - dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst - (MSTRONG: match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) + dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst + (MSTRONG: match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) (NGOTO: is_goto ib = false) - : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) + : match_states (Some ib) (RTL.State st f sp pcR1 rs1 m1) (State st' f' sp pcB0 rs0 m0) | match_states_call st st' f f' args m (STACKS: list_forall2 match_stackframes st st') @@ -260,17 +260,48 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. +(** * Match strong state property + +Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2). +Two possible executions: + +<< + + **ib2 is a Bgoto (left side):** + + RTL state MSS1 BTL state + [pcR1,rs1,m1] -------------------------- [ib1,pcB0,rs0,m0] + | | + | | + | | BTL_STEP + | | + | | + RTL_STEP | *E0 [ib2,pc=(Bgoto succ),rs2,m2] + | / | + | MSS2 / | + | _________________/ | BTL_GOTO + | / | + | / GOAL: match_states | + [pcR2,rs2,m2] ------------------------ [ib?,pc=succ,rs2,m2] + + + **ib2 is any other instruction (right side):** + +See explanations of opt_simu below. + +>> +*) Lemma match_strong_state_simu - dupmap st st' f f' sp rs m rs0 m0 rs1 m1 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n - (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) E0 (RTL.State st f sp pcR2 rs1 m1)) - (MSS1 : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst) - (MSS2 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false) + 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)) + (MSS1 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst) + (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' - /\ match_states oib' (RTL.State st f sp pcR2 rs1 m1) 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 rs1 m1) (State st' f' sp pcB0 rs0 m0)). + /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)). Proof. destruct (is_goto ib2) eqn:GT. destruct ib2; try destruct fi; try discriminate. @@ -427,7 +458,7 @@ Two possible executions: << - **Last instruction:** + **Last instruction (left side):** RTL state match_states BTL state s1 ------------------------------------ s2 @@ -437,7 +468,7 @@ Two possible executions: s1' ----------------------------------- s2' - **Middle instruction:** + **Middle instruction (right side):** RTL state match_states [oib] BTL state s1 ------------------------------------ s2 -- cgit