ascii simu

1 files changed, 48 insertions, 17 deletions

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