diff options
Diffstat (limited to 'mppa_k1c/abstractbb')
| -rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 30 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/DepExample.v | 151 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/DepExampleDemo.v | 400 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/DepExampleEqTest.v | 334 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/DepExampleParallelTest.v | 166 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 60 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 30 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 10 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpPrelude.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 178 |
10 files changed, 163 insertions, 1200 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 904fb72c..3023ad8a 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -2,19 +2,19 @@ *) -Module Type ResourceNames. +Module Type PseudoRegisters. Parameter t: Type. Parameter eq_dec: forall (x y: t), { x = y } + { x<>y }. -End ResourceNames. +End PseudoRegisters. (** * Parameters of the language of Basic Blocks *) Module Type LangParam. -Declare Module R: ResourceNames. +Declare Module R: PseudoRegisters. Parameter value: Type. @@ -55,18 +55,18 @@ Definition assign (m: mem) (x:R.t) (v: value): mem := fun y => if R.eq_dec x y then v else m y. Inductive exp := - | Name (x:R.t) + | PReg (x:R.t) | Op (o:op) (le: list_exp) | Old (e: exp) with list_exp := | Enil | Econs (e:exp) (le:list_exp) | LOld (le: list_exp) - . +. Fixpoint exp_eval (e: exp) (m old: mem): option value := match e with - | Name x => Some (m x) + | PReg x => Some (m x) | Op o le => match list_exp_eval le m old with | Some lv => op_eval ge o lv @@ -85,25 +85,25 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) := | LOld le => list_exp_eval le old old end. -Definition macro := list (R.t * exp). (* = a sequence of assignments *) +Definition inst := list (R.t * exp). (* = a sequence of assignments *) -Fixpoint macro_run (i: macro) (m old: mem): option mem := +Fixpoint inst_run (i: inst) (m old: mem): option mem := match i with | nil => Some m | (x, e)::i' => match exp_eval e m old with - | Some v' => macro_run i' (assign m x v') old + | Some v' => inst_run i' (assign m x v') old | None => None end end. -Definition bblock := list macro. +Definition bblock := list inst. Fixpoint run (p: bblock) (m: mem): option mem := match p with | nil => Some m | i::p' => - match macro_run i m m with + match inst_run i m m with | Some m' => run p' m' | None => None end @@ -166,10 +166,10 @@ Qed. Definition bblock_equiv (p1 p2: bblock): Prop := forall m, res_eq (run p1 m) (run p2 m). -Lemma alt_macro_equiv_refl i old1 old2: +Lemma alt_inst_equiv_refl i old1 old2: (forall x, old1 x = old2 x) -> forall m1 m2, (forall x, m1 x = m2 x) -> - res_eq (macro_run i m1 old1) (macro_run i m2 old2). + res_eq (inst_run i m1 old1) (inst_run i m2 old2). Proof. intro H; induction i as [ | [x e]]; simpl; eauto. intros m1 m2 H1. erewrite exp_equiv; eauto. @@ -181,9 +181,9 @@ Qed. Lemma alt_bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). Proof. induction p as [ | i p']; simpl; eauto. - intros m1 m2 H; lapply (alt_macro_equiv_refl i m1 m2); auto. + intros m1 m2 H; lapply (alt_inst_equiv_refl i m1 m2); auto. intros X; lapply (X m1 m2); auto; clear X. - destruct (macro_run i m1 m1); simpl. + destruct (inst_run i m1 m1); simpl. - intros [m3 [H1 H2]]; rewrite H1; simpl; auto. - intros H1; rewrite H1; simpl; auto. Qed. diff --git a/mppa_k1c/abstractbb/DepExample.v b/mppa_k1c/abstractbb/DepExample.v deleted file mode 100644 index a239e24f..00000000 --- a/mppa_k1c/abstractbb/DepExample.v +++ /dev/null @@ -1,151 +0,0 @@ -(** Specification of the example illustrating how to use ImpDep. *) - -Require Export ZArith. - -Require Export ZArith. -Require Export List. -Export ListNotations. - -(* Syntax *) - -Definition reg := positive. - -Inductive operand := - | Imm (i:Z) - | Reg (r:reg) - . - -Inductive arith_op := ADD | SUB | MUL. - -Inductive inst := - | MOVE (dest: reg) (src: operand) - | ARITH (dest: reg) (op: arith_op) (src1 src2: operand) - | LOAD (dest base: reg) (offset: operand) - | STORE (src base: reg) (offset: operand) - | MEMSWAP (r base: reg) (offset: operand) - . - -Definition bblock := list inst. - -(* Semantics *) - -Definition value := Z. - -Definition addr := positive. - -Definition mem := addr -> value. - -Definition assign (m: mem) (x:addr) (v: value) := - fun y => if Pos.eq_dec x y then v else (m y). - -Definition regmem := reg -> value. - -Record state := { sm: mem; rm: regmem }. - -Definition operand_eval (x: operand) (rm: regmem): value := - match x with - | Imm i => i - | Reg r => rm r - end. - -Definition arith_op_eval (o: arith_op): value -> value -> value := - match o with - | ADD => Z.add - | SUB => Z.sub - | MUL => Z.mul - end. - -Definition get_addr (base:reg) (offset:operand) (rm: regmem): option addr := - let b := rm base in - let ofs := operand_eval offset rm in - match Z.add b ofs with - | Zpos p => Some p - | _ => None - end. - -(* two-state semantics -- dissociating read from write access. - - all read access on [sin] state - - all register write access modifies [sout] state - - all memory write access modifies [sin] state - => useful for parallel semantics - NB: in this parallel semantics -- there is at most one STORE by bundle - which is non-deterministically chosen... -*) -Definition sem_inst (i: inst) (sin sout: state): option state := - match i with - | MOVE dest src => - let v := operand_eval src (rm sin) in - Some {| sm := sm sout; - rm := assign (rm sout) dest v |} - | ARITH dest op src1 src2 => - let v1 := operand_eval src1 (rm sin) in - let v2 := operand_eval src2 (rm sin) in - let v := arith_op_eval op v1 v2 in - Some {| sm := sm sout; - rm := assign (rm sout) dest v |} - | LOAD dest base offset => - match get_addr base offset (rm sin) with - | Some srce => - Some {| sm := sm sout; - rm := assign (rm sout) dest (sm sin srce) |} - | None => None - end - | STORE srce base offset => - match get_addr base offset (rm sin) with - | Some dest => - Some {| sm := assign (sm sin) dest (rm sin srce); - rm := rm sout |} - | None => None - end - | MEMSWAP x base offset => - match get_addr base offset (rm sin) with - | Some ad => - Some {| sm := assign (sm sin) ad (rm sin x); - rm := assign (rm sout) x (sm sin ad) |} - | None => None - end - end. - -Local Open Scope list_scope. - -(** usual sequential semantics *) -Fixpoint sem_bblock (p: bblock) (s: state): option state := - match p with - | nil => Some s - | i::p' => - match sem_inst i s s with - | Some s' => sem_bblock p' s' - | None => None - end - end. - -Definition state_equiv (s1 s2: state): Prop := - (forall x, sm s1 x = sm s2 x) /\ - (forall x, rm s1 x = rm s2 x). - -(* equalities on bblockram outputs *) -Definition res_equiv (os1 os2: option state): Prop := - match os1 with - | Some s1 => exists s2, os2 = Some s2 /\ state_equiv s1 s2 - | None => os2 = None - end. - - -Definition bblock_equiv (p1 p2: bblock): Prop := - forall s, res_equiv (sem_bblock p1 s) (sem_bblock p2 s). - -(** parallel semantics with in-order writes *) -Fixpoint sem_bblock_par_iw (p: bblock) (sin sout: state): option state := - match p with - | nil => Some sout - | i::p' => - match sem_inst i sin sout with - | Some sout' => sem_bblock_par_iw p' sin sout' - | None => None - end - end. - -(** parallelism semantics with arbitrary order writes *) -Require Import Sorting.Permutation. - -Definition sem_bblock_par (p: bblock) (sin: state) (sout: option state) := exists p', res_equiv sout (sem_bblock_par_iw p' sin sin) /\ Permutation p p'. diff --git a/mppa_k1c/abstractbb/DepExampleDemo.v b/mppa_k1c/abstractbb/DepExampleDemo.v deleted file mode 100644 index 74e8f35e..00000000 --- a/mppa_k1c/abstractbb/DepExampleDemo.v +++ /dev/null @@ -1,400 +0,0 @@ -(** Demo of the example illustrating how to use ImpDep. *) - -Require Import DepExampleEqTest. -Require Import Bool. - -Open Scope Z_scope. - -Module EqTests. - -Section TESTS. - -Variable ge: P.genv. - -(**** TESTS DRIVER ! ****) - -Record test_input := { - name: pstring; - expected: bool; - verbose: bool; - p1: bblock; - p2: bblock; -}. - -Definition run1 (t: test_input): ?? unit := - print ((name t) +; " =>");; - DO result <~ bblock_eq_test ge (verbose t) (p1 t) (p2 t);; - assert_b (eqb result (expected t)) "UNEXPECTED RESULT";; - if expected t - then println " SUCCESS" - else RET tt (* NB: in this case - bblock_eq_test is expected to have print an ERROR mesg *) - . - -Local Hint Resolve eqb_prop. - -Lemma run1_correctness (t: test_input): - WHEN run1 t ~> _ THEN (expected t)=true -> bblock_equiv (p1 t) (p2 t). -Proof. - unfold run1; destruct t; simpl; wlp_simplify; subst. -Qed. -Global Opaque run1. -Hint Resolve run1_correctness: wlp. - -Fixpoint run_all (l: list test_input): ?? unit := - match l with - | nil => RET tt - | t::l' => - println "" ;; (* SOME SPACES ! *) - run1 t;; - run_all l' - end. - -Lemma run_all_correctness l: - WHEN run_all l ~> _ THEN (forall t, List.In t l -> (expected t)=true -> bblock_equiv (p1 t) (p2 t)). -Proof. - induction l; simpl; wlp_simplify; subst; auto. -Qed. -Global Opaque run_all. - -(**** TESTS ****) - -Definition move (dst src: reg) := MOVE dst (Reg src). -Definition add_imm (dst src: reg) (z:Z) := ARITH dst ADD (Reg src) (Imm z). -Definition incr (r: reg) (z:Z) := add_imm r r z. -Definition add (dst src1 src2: reg) := ARITH dst ADD (Reg src1) (Reg src2). - -Definition load (dst src:reg) (ofs:Z) := LOAD dst src (Imm ofs). -Definition store (src dst:reg) (ofs:Z) := STORE src dst (Imm ofs). -Definition memswap (r base:reg) (ofs:Z) := MEMSWAP r base (Imm ofs). - -Definition R1: reg := 1%positive. -Definition R2: reg := 2%positive. -Definition R3: reg := 3%positive. -Definition R4: reg := 4%positive. - - -Definition demo: ?? unit := run_all [ - - {| name:="move_ok" ; - expected:=true; - verbose:=true; - p1:=[ move R2 R1; move R3 R1 ]; - p2:=[ move R3 R1; move R2 R3 ]; - |} ; - {| name:="move_ko" ; - expected:=false; - verbose:=true; - p1:=[ move R2 R1; move R3 R1 ]; - p2:=[ move R3 R1 ]; - |} ; - - {| name:="add_load_RAR_ok" ; - expected:=true; - verbose:=true; - p1:=[ add_imm R1 R2 5; move R4 R2; load R3 R2 2 ]; - p2:=[ load R3 R2 2; add_imm R1 R2 5; move R4 R2 ]; |} ; - - {| name:="add_load_RAW_ko"; - expected:=false; - verbose:=true; - p1:=[ add_imm R1 R2 5; move R4 R2; load R3 R1 2 ]; - p2:=[ load R3 R1 2; add_imm R1 R2 5; move R4 R2 ]; |} ; - - {| name:="add_load_WAW_ko"; - expected:=false; - verbose:=true; - p1:=[ add_imm R3 R2 5; move R4 R2; load R3 R1 2 ]; - p2:=[ load R3 R1 2; add_imm R3 R2 5; move R4 R2 ]; |} ; - - {| name:="memswap_ok1"; - expected:=true; - verbose:=true; - p1:=[ add_imm R1 R2 5; memswap R3 R2 2 ]; - p2:=[ memswap R3 R2 2; add_imm R1 R2 5 ]; |} ; - - {| name:="memswap_ok2" ; - expected:=true; - verbose:=true; - p1:=[ load R1 R2 2; store R3 R2 2; move R3 R1]; - p2:=[ memswap R3 R2 2 ; move R1 R3 ]; - |} ; - - {| name:="memswap_ko" ; - expected:=false; - verbose:=true; - p1:=[ load R3 R2 2; store R3 R2 2]; - p2:=[ memswap R3 R2 2 ]; - |} -]. - - -Fixpoint repeat_aux (n:nat) (rev_body next: bblock): bblock := - match n with - | O => next - | (S n) => repeat_aux n rev_body (List.rev_append rev_body next) - end. - -Definition repeat n body next := repeat_aux n (List.rev_append body []) next. - - -Definition inst1 := add R1 R1 R2. - -(* NB: returns [inst1^10; next] *) -Definition dummy1 next:= repeat 10%nat [inst1] next. - -Definition main: ?? unit := run_all [ - - {| name:="move_never_skips1" ; - expected:=false; - verbose:=false; - p1:=[ move R2 R2 ]; - p2:=[ ]; - |} ; - - {| name:="move_compress_ok" ; - expected:=true; - verbose:=false; - p1:=[ move R1 R2; move R2 R1; MOVE R1 (Imm 7) ]; - p2:=[ MOVE R1 (Imm 7); move R2 R2 ]; - |} ; - - {| name:="move_never_skip2" ; - expected:=false; - verbose:=false; - p1:=[ move R1 R2; move R2 R1; MOVE R1 (Imm 7) ]; - p2:=[ MOVE R1 (Imm 7) ]; - |} ; - - {| name:="R2_RAR_ok1"; - expected:=true; - verbose:=false; - p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ]; - p2:=load R3 R2 2::store R3 R4 7::(dummy1 nil) |} ; - {| name:="R2_RAR_ok2"; - expected:=true; - verbose:=false; - p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ]; - p2:=load R3 R2 2::(dummy1 [store R3 R4 7]) |} ; - {| name:="R2_RAR_ok3"; - expected:=true; - verbose:=false; - p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ]; - p2:=load R3 R2 2::(repeat 4%nat [inst1;inst1] [store R3 R4 7; inst1; inst1]) |} ; - {| name:="bad_register_name_ko"; - expected:=false; - verbose:=false; - p1:=dummy1 [ load R3 R2 2 ]; - p2:=dummy1 [ load R3 R3 2 ] |} ; - {| name:="bad_instruction_ko"; - expected:=false; - verbose:=false; - p1:=dummy1 [ load R3 R2 2 ]; - p2:=dummy1 [ store R3 R2 2 ] |} ; - {| name:="incompleteness_ko"; - expected:=false; - verbose:=false; - p1:=dummy1 [ load R3 R2 2 ]; - p2:=[inst1; load R3 R2 2] |} ; - - - {| name:="R2_WAR_ko"; - expected:=false; - verbose:=false; - p1:=dummy1 [ load R2 R3 2 ]; - p2:=load R2 R3 2::(dummy1 nil) |} ; - {| name:="bad_register_name_ko2"; - expected:=false; - verbose:=false; - p1:=dummy1 [ load R2 R3 2 ]; - p2:=load R3 R2 2::(dummy1 nil) |} ; - - - {| name:="load_RAR_ok1"; - expected:=true; - verbose:=false; - p1:=[ load R1 R2 2; load R3 R4 5]; - p2:=[ load R3 R4 5; load R1 R2 2]; |} ; - {| name:="load_RAR_ok2"; - expected:=true; - verbose:=false; - p1:=[ load R1 R2 2; load R3 R2 5]; - p2:=[ load R3 R2 5; load R1 R2 2]; |} ; - {| name:="load_WAW_ko"; - expected:=false; - verbose:=false; - p1:=[ load R1 R2 2; load R1 R4 5]; - p2:=[ load R1 R4 5; load R1 R2 2]; |} ; - {| name:="load_store_WAR_ko"; - expected:=false; - verbose:=false; - p1:=[ load R1 R2 2; store R3 R4 5]; - p2:=[ store R3 R4 5; load R1 R2 2]; |} - - ]. - -Definition incr_R1_5 := incr R1 5. -Definition incr_R2_3 := incr R2 3. - -Definition big_test (bigN:nat) (name: pstring): ?? unit := - println "";; - println("---- Time of bigtest " +; name);; - timer(run_all, [ - - {| name:="big_test_ok1"; - expected:=true; - verbose:=false; - p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3]; - p2:=repeat bigN [incr_R1_5] (repeat (S bigN) [incr_R2_3] nil) |} ; - {| name:="big_test_ok2"; - expected:=true; - verbose:=false; - p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3]; - p2:=repeat bigN [incr_R2_3;incr_R1_5] [incr_R2_3] |} ; - {| name:="big_test_ok3"; - expected:=true; - verbose:=false; - p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3]; - p2:=repeat (S bigN) [incr_R2_3] (repeat bigN [incr_R1_5] nil) |} ; - {| name:="big_test_ko1"; - expected:=false; - verbose:=false; - p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3]; - p2:=repeat bigN [incr_R1_5] (repeat bigN [incr_R2_3] nil) |} ; - {| name:="big_test_ko2"; - expected:=false; - verbose:=false; - p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3]; - p2:=repeat (S bigN) [incr_R1_5] (repeat bigN [incr_R2_3] nil) |} - - ]). - -Fixpoint big_tests (l:list (nat * string)) := - match l with - | nil => RET tt - | (x,s)::l' => big_test x s;; big_tests l' - end. - -Local Open Scope nat_scope. -Local Open Scope string_scope. - -Definition big_runs: ?? unit := - big_tests [(2500, "2500"); (5000, "5000"); (10000, "10000"); (20000, "20000")]. - - -End EqTests. - - -Require Import DepExampleParallelTest. - -Module ParaTests. - - -(**** TESTS DRIVER ! ****) - -Record test_input := { - name: pstring; - expected: bool; - bundle: bblock; -}. - -Definition run1 (t: test_input): ?? unit := - print ((name t) +; " =>");; - assert_b (eqb (bblock_is_para (bundle t)) (expected t)) "UNEXPECTED RESULT";; - if expected t - then println " SUCCESS" - else println " FAILED (as expected)" - . - -Local Hint Resolve eqb_prop. - -Definition correct_bundle p := forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)). - -Lemma run1_correctness (t: test_input): - WHEN run1 t ~> _ THEN (expected t)=true -> correct_bundle (bundle t). -Proof. - unfold run1; destruct t; simpl; wlp_simplify; subst. - - unfold correct_bundle; intros; apply bblock_is_para_correct; auto. - - discriminate. -Qed. -Global Opaque run1. -Hint Resolve run1_correctness: wlp. - -Fixpoint run_all (l: list test_input): ?? unit := - match l with - | nil => RET tt - | t::l' => - run1 t;; - run_all l' - end. - -Lemma run_all_correctness l: - WHEN run_all l ~> _ THEN (forall t, List.In t l -> (expected t)=true -> correct_bundle (bundle t)). -Proof. - induction l; simpl; wlp_simplify; subst; auto. -Qed. -Global Opaque run_all. - -(**** TESTS ****) - -Definition add_imm (dst src: reg) (z:Z) := ARITH dst ADD (Reg src) (Imm z). - -Definition load (dst src:reg) (ofs:Z) := LOAD dst src (Imm ofs). -Definition store (src dst:reg) (ofs:Z) := STORE src dst (Imm ofs). -Definition memswap (r base:reg) (ofs:Z) := MEMSWAP r base (Imm ofs). - -Definition R1: reg := 1%positive. -Definition R2: reg := 2%positive. -Definition R3: reg := 3%positive. -Definition R4: reg := 4%positive. -Definition R5: reg := 5%positive. -Definition R6: reg := 5%positive. - - -Definition main: ?? unit := - println "";; - println "-- Parallel Checks --";; - run_all [ - {| name:="test_war_ok"; - expected:=true; - bundle:=[add_imm R1 R2 2;add_imm R2 R2 3] - |}; - {| name:="test_raw_ko"; - expected:=false; - bundle:=[add_imm R1 R2 2;add_imm R2 R1 3] - |}; - {| name:="test_waw_ko"; - expected:=false; - bundle:=[add_imm R1 R2 2;add_imm R1 R2 3] - |}; - {| name:="test_war_load_store_ok"; - expected:=true; - bundle:=[load R1 R2 2;load R2 R3 3; store R3 R4 4] - |}; - {| name:="test_raw_load_store_ko"; - expected:=false; - bundle:=[load R1 R2 2;store R5 R4 4;load R2 R3 3] - |}; - {| name:="test_waw_load_store_ko"; - expected:=false; - bundle:=[load R1 R2 2;store R3 R2 3;store R5 R4 4] - |}; - {| name:="test_arith_load_store_ok"; - expected:=true; - bundle:=[load R1 R2 2; add_imm R2 R4 3; load R3 R6 3; add_imm R4 R4 3; store R6 R5 4; add_imm R6 R6 7] - |} - ]. - -End ParaTests. - -(*************************) -(* Extraction directives *) - -Require Import ExtrOcamlString. -Require Import ExtrOcamlBasic. - -Import ImpConfig. - -Extraction Blacklist List String. - -Separate Extraction BinIntDef EqTests ParaTests. - diff --git a/mppa_k1c/abstractbb/DepExampleEqTest.v b/mppa_k1c/abstractbb/DepExampleEqTest.v deleted file mode 100644 index a633ee07..00000000 --- a/mppa_k1c/abstractbb/DepExampleEqTest.v +++ /dev/null @@ -1,334 +0,0 @@ -(** Implementation of the example illustrating how to use ImpDep. *) - -Require Export DepExample. -Require Export Impure.ImpIO. -Export Notations. - -Require Import ImpDep. - -Open Scope impure. - -Module P<: ImpParam. - -Module R := Pos. - -Definition genv := unit. - -Section IMP. - -Inductive value_wrap := - | Std (v:value) (* value = DepExample.value *) - | Mem (m:mem) - . - -Inductive op_wrap := - (* constants *) - | Imm (i:Z) - (* arithmetic operation *) - | ARITH (op: arith_op) - | LOAD - | STORE - . - -Definition op_eval (ge: genv) (op: op_wrap) (l:list value_wrap): option value_wrap := - match op, l with - | Imm i, [] => Some (Std i) - | ARITH op, [Std v1; Std v2] => Some (Std (arith_op_eval op v1 v2)) - | LOAD, [Mem m; Std base; Std offset] => - match (Z.add base offset) with - | Zpos srce => Some (Std (m srce)) - | _ => None - end - | STORE, [Mem m; Std srce; Std base; Std offset] => - match (Z.add base offset) with - | Zpos dest => Some (Mem (assign m dest srce)) - | _ => None - end - | _, _ => None - end. - - -Definition value:=value_wrap. -Definition op:=op_wrap. - -Definition op_eq (o1 o2: op_wrap): ?? bool := - match o1, o2 with - | Imm i1, Imm i2 => phys_eq i1 i2 - | ARITH o1, ARITH o2 => phys_eq o1 o2 - | LOAD, LOAD => RET true - | STORE, STORE => RET true - | _, _ => RET false - end. - -Lemma op_eq_correct o1 o2: - WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. -Proof. - destruct o1, o2; wlp_simplify; congruence. -Qed. - -End IMP. -End P. - - -Module L <: ISeqLanguage with Module LP:=P. - -Module LP:=P. - -Include MkSeqLanguage P. - -End L. - - -Module IDT := ImpDepTree L ImpPosDict. - -Section SECT. -Variable ge: P.genv. - -(** Compilation from DepExample to L *) - -Definition the_mem: P.R.t := 1. -Definition reg_map (r: reg): P.R.t := Pos.succ r. - -Coercion L.Name: P.R.t >-> L.exp. - -Definition comp_op (o:operand): L.exp := - match o with - | Imm i => L.Op (P.Imm i) L.Enil - | Reg r => reg_map r - end. - -Definition comp_inst (i: inst): L.macro := - match i with - | MOVE dest src => - [ (reg_map dest, (comp_op src)) ] - | ARITH dest op src1 src2 => - [ (reg_map dest, L.Op (P.ARITH op) (L.Econs (comp_op src1) (L.Econs (comp_op src2) L.Enil))) ] - | LOAD dest base offset => - [ (reg_map dest, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))) ] - | STORE srce base offset => - [ (the_mem, L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map srce) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil))))) ] - | MEMSWAP x base offset => - [ (reg_map x, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))); - (the_mem, L.Old (L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map x) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))))) ] - end. - -Fixpoint comp_bblock (p: bblock): L.bblock := - match p with - | nil => nil - | i::p' => (comp_inst i)::(comp_bblock p') - end. - -(** Correctness proof of the compiler *) - -Lemma the_mem_separation: forall r, reg_map r <> the_mem. -Proof. - intros r; apply Pos.succ_not_1. -Qed. - -Lemma reg_map_separation: forall r1 r2, r1 <> r2 -> reg_map r1 <> reg_map r2. -Proof. - unfold reg_map; intros r1 r2 H1 H2; lapply (Pos.succ_inj r1 r2); auto. -Qed. - -Local Hint Resolve the_mem_separation reg_map_separation. - -Definition match_state (s: state) (m:L.mem): Prop := - m the_mem = P.Mem (sm s) /\ forall r, m (reg_map r) = P.Std (rm s r). - -Definition trans_state (s: state): L.mem := - fun x => - if Pos.eq_dec x the_mem - then P.Mem (sm s) - else P.Std (rm s (Pos.pred x)). - -Lemma match_trans_state (s:state): match_state s (trans_state s). -Proof. - unfold trans_state; constructor 1. - - destruct (Pos.eq_dec the_mem the_mem); try congruence. - - intros r; destruct (Pos.eq_dec (reg_map r) the_mem). - * generalize the_mem_separation; subst; congruence. - * unfold reg_map; rewrite Pos.pred_succ. auto. -Qed. - -Definition match_option_state (os: option state) (om:option L.mem): Prop := - match os with - | Some s => exists m, om = Some m /\ match_state s m - | None => om = None - end. - -Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval ge (comp_op o) m old = Some (P.Std (operand_eval o (rm s))). -Proof. - destruct 1 as [H1 H2]; destruct o; simpl; auto. - rewrite H2; auto. -Qed. - -Lemma comp_bblock_correct_aux p: forall s m, match_state s m -> match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) m). -Proof. - induction p as [| i p IHp]; simpl; eauto. - intros s m H; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl. - - (* MOVE *) - apply IHp. - destruct H as [H1 H2]; constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* ARITH *) - apply IHp. - destruct H as [H1 H2]; constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* LOAD *) - destruct H as [H1 H2]. - rewrite H1, H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* STORE *) - destruct H as [H1 H2]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl; auto. - + intros r; rewrite L.assign_diff; auto. - - (* MEMSWAP *) - destruct H as [H1 H2]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl; auto. - intros r0; rewrite L.assign_diff; auto. - unfold assign; destruct (Pos.eq_dec r r0). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. -Qed. - -Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) (trans_state s)). -Proof. - eapply comp_bblock_correct_aux. apply match_trans_state. -Qed. - -Lemma state_equiv_from_match (s1 s2: state) (m: L.mem) : - (match_state s1 m) -> (match_state s2 m) -> (state_equiv s1 s2). -Proof. - unfold state_equiv, match_state. intuition. - - congruence. - - assert (P.Std (rm s1 x) = P.Std (rm s2 x)); congruence. -Qed. - -Definition match_option_stateX (om:option L.mem) (os:option state): Prop := - match om with - | Some m => exists s, os = Some s /\ match_state s m - | None => os = None - end. - -Local Hint Resolve state_equiv_from_match. - -Lemma res_equiv_from_match (os1 os2: option state) (om: option L.mem): - (match_option_state os1 om) -> (match_option_stateX om os2) -> (res_equiv os1 os2). -Proof. - destruct os1 as [s1|]; simpl. - - intros [m [H1 H2]]; subst; simpl. - intros [s2 [H3 H4]]; subst; simpl. - eapply ex_intro; intuition eauto. - - intro; subst; simpl; auto. -Qed. - - -Lemma match_option_state_intro_X om os: match_option_state os om -> match_option_stateX om os. -Proof. - destruct os as [s | ]; simpl. - - intros [m [H1 H2]]. subst; simpl. eapply ex_intro; intuition eauto. - - intros; subst; simpl; auto. -Qed. - - -Lemma match_from_res_eq om1 om2 os: - L.res_eq om2 om1 -> match_option_stateX om1 os -> match_option_stateX om2 os. -Proof. - destruct om2 as [m2 | ]; simpl. - - intros [m [H1 H2]]. subst; simpl. - intros [s [H3 H4]]; subst; simpl. - eapply ex_intro; intuition eauto. - unfold match_state in * |- *. - intuition (rewrite H2; auto). - - intros; subst; simpl; auto. -Qed. - -Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv ge (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2. -Proof. - unfold L.bblock_equiv, bblock_equiv. - intros; eapply res_equiv_from_match. - apply comp_bblock_correct. - eapply match_from_res_eq. eauto. - apply match_option_state_intro_X. - apply comp_bblock_correct. -Qed. - - - - -(* NB: pretty-printing functions below only mandatory for IDT.verb_bblock_eq_test *) -Local Open Scope string_scope. - -Definition string_of_name (x: P.R.t): ?? pstring := - match x with - | xH => RET (Str ("the_mem")) - | _ as x => - DO s <~ string_of_Z (Zpos (Pos.pred x)) ;; - RET ("R" +; s) - end. - -Definition string_of_op (op: P.op): ?? pstring := - match op with - | P.Imm i => - DO s <~ string_of_Z i ;; - RET s - | P.ARITH ADD => RET (Str "ADD") - | P.ARITH SUB => RET (Str "SUB") - | P.ARITH MUL => RET (Str "MUL") - | P.LOAD => RET (Str "LOAD") - | P.STORE => RET (Str "STORE") - end. - -Definition bblock_eq_test (verb: bool) (p1 p2: bblock) : ?? bool := - if verb then - IDT.verb_bblock_eq_test string_of_name string_of_op ge (comp_bblock p1) (comp_bblock p2) - else - IDT.bblock_eq_test ge (comp_bblock p1) (comp_bblock p2). - -Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp. - - -Theorem bblock_eq_test_correct verb p1 p2 : - WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2. -Proof. - wlp_simplify. -Qed. -Global Opaque bblock_eq_test. -Hint Resolve bblock_eq_test_correct: wlp. - -End SECT. -(* TEST: we can coerce this bblock_eq_test into a pure function (even if this is a little unsafe). *) -(* -Import UnsafeImpure. - -Definition pure_eq_test v (p1 p2: bblock) : bool := unsafe_coerce (bblock_eq_test v p1 p2). - -Theorem pure_eq_test_correct v p1 p2 : - pure_eq_test v p1 p2 = true -> bblock_equiv p1 p2. -Proof. - unfold pure_eq_test. intros; eapply bblock_eq_test_correct. - - apply unsafe_coerce_not_really_correct; eauto. - - eauto. -Qed. -*)
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/DepExampleParallelTest.v b/mppa_k1c/abstractbb/DepExampleParallelTest.v deleted file mode 100644 index 35b44683..00000000 --- a/mppa_k1c/abstractbb/DepExampleParallelTest.v +++ /dev/null @@ -1,166 +0,0 @@ -Require Import DepExampleEqTest. -Require Import Parallelizability. - -Module PChk := ParallelChecks L PosResourceSet. - -Definition bblock_is_para (p: bblock) : bool := - PChk.is_parallelizable (comp_bblock p). - -Local Hint Resolve the_mem_separation reg_map_separation. - -Section SEC. -Variable ge: P.genv. - -(* Actually, almost the same proof script than [comp_bblock_correct_aux] ! - We could definitely factorize the proof through a lemma on compilation to macros. -*) -Lemma comp_bblock_correct_para_iw p: forall sin sout min mout, - match_state sin min -> - match_state sout mout -> - match_option_state (sem_bblock_par_iw p sin sout) (PChk.prun_iw ge (comp_bblock p) mout min). -Proof. - induction p as [|i p IHp]; simpl; eauto. - intros sin sout min mout Hin Hout; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl. - - (* MOVE *) - apply IHp; auto. - destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* ARITH *) - apply IHp; auto. - destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* LOAD *) - destruct Hin as [H1 H2]; destruct Hout as [H3 H4]. - rewrite H1, H2; simpl. - unfold get_addr. - destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto. - apply IHp. { constructor 1; auto. } - constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* STORE *) - destruct Hin as [H1 H2]; destruct Hout as [H3 H4]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto. - apply IHp. { constructor 1; auto. } - constructor 1; simpl; auto. - intros r; rewrite L.assign_diff; auto. - - (* MEMSWAP *) - destruct Hin as [H1 H2]; destruct Hout as [H3 H4]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto. - apply IHp. { constructor 1; auto. } - constructor 1; simpl; auto. - + intros r0; rewrite L.assign_diff; auto. - unfold assign; destruct (Pos.eq_dec r r0). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. -Qed. - -Local Hint Resolve match_trans_state. - -Definition trans_option_state (os: option state): option L.mem := - match os with - | Some s => Some (trans_state s) - | None => None - end. - -Lemma match_trans_option_state os: match_option_state os (trans_option_state os). -Proof. - destruct os; simpl; eauto. -Qed. - -Local Hint Resolve match_trans_option_state comp_bblock_correct match_option_state_intro_X match_from_res_eq res_equiv_from_match. - -Lemma is_mem_reg (x: P.R.t): x=the_mem \/ exists r, x=reg_map r. -Proof. - case (Pos.eq_dec x the_mem); auto. - unfold the_mem, reg_map; constructor 2. - eexists (Pos.pred x). rewrite Pos.succ_pred; auto. -Qed. - -Lemma res_eq_from_match (os: option state) (om1 om2: option L.mem): - (match_option_stateX om1 os) -> (match_option_state os om2) -> (L.res_eq om1 om2). -Proof. - destruct om1 as [m1|]; simpl. - - intros (s & H1 & H2 & H3); subst; simpl. - intros (m2 & H4 & H5 & H6); subst; simpl. - eapply ex_intro; intuition eauto. - destruct (is_mem_reg x) as [H|(r & H)]; subst; congruence. - - intro; subst; simpl; auto. -Qed. - -(* We use axiom of functional extensionality ! *) -Require Coq.Logic.FunctionalExtensionality. - -Lemma match_from_res_equiv os1 os2 om: - res_equiv os2 os1 -> match_option_state os1 om -> match_option_state os2 om. -Proof. - destruct os2 as [s2 | ]; simpl. - - intros (s & H1 & H2 & H3). subst; simpl. - intros (m & H4 & H5 & H6); subst; simpl. - eapply ex_intro; intuition eauto. - constructor 1. - + rewrite H5; apply f_equal; eapply FunctionalExtensionality.functional_extensionality; auto. - + congruence. - - intros; subst; simpl; auto. -Qed. - - -Require Import Sorting.Permutation. - -Local Hint Constructors Permutation. - -Lemma comp_bblock_Permutation p p': Permutation p p' -> Permutation (comp_bblock p) (comp_bblock p'). -Proof. - induction 1; simpl; eauto. -Qed. - -Lemma comp_bblock_Permutation_back p1 p1': Permutation p1 p1' -> - forall p, p1=comp_bblock p -> - exists p', p1'=comp_bblock p' /\ Permutation p p'. -Proof. - induction 1; simpl; eauto. - - destruct p as [|i p]; simpl; intro X; inversion X; subst. - destruct (IHPermutation p) as (p' & H1 & H2); subst; auto. - eexists (i::p'). simpl; eauto. - - destruct p as [|i1 p]; simpl; intro X; inversion X as [(H & H1)]; subst; clear X. - destruct p as [|i2 p]; simpl; inversion_clear H1. - eexists (i2::i1::p). simpl; eauto. - - intros p H1; destruct (IHPermutation1 p) as (p' & H2 & H3); subst; auto. - destruct (IHPermutation2 p') as (p'' & H4 & H5); subst; eauto. -Qed. - -Local Hint Resolve comp_bblock_Permutation res_eq_from_match match_from_res_equiv comp_bblock_correct_para_iw. - -Lemma bblock_par_iff_prun p s os': - sem_bblock_par p s os' <-> PChk.prun ge (comp_bblock p) (trans_state s) (trans_option_state os'). -Proof. - unfold sem_bblock_par, PChk.prun. constructor 1. - - intros (p' & H1 & H2). - eexists (comp_bblock p'); intuition eauto. - - intros (p' & H1 & H2). - destruct (comp_bblock_Permutation_back _ _ H2 p) as (p0 & H3 & H4); subst; auto. - eexists p0; constructor 1; eauto. -Qed. - -Theorem bblock_is_para_correct p: - bblock_is_para p = true -> forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)). -Proof. - intros H; generalize (PChk.is_parallelizable_correct ge _ H); clear H. - intros H s os'. - rewrite bblock_par_iff_prun, H. - constructor; eauto. -Qed. - -End SEC.
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index 353e9160..bfe79d42 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -9,9 +9,9 @@ Require Setoid. (* in order to rewrite <-> *) Require Export AbstractBasicBlocksDef. -Module Type ResourceDictionary. +Module Type PseudoRegDictionary. -Declare Module R: ResourceNames. +Declare Module R: PseudoRegisters. Parameter t: Type -> Type. @@ -30,12 +30,12 @@ Parameter empty: forall {A}, t A. Parameter empty_spec: forall A x, get (empty (A:=A)) x = None. -End ResourceDictionary. +End PseudoRegDictionary. (** * Computations of "bblock" Dependencies and application to the equality test *) -Module DepTree (L: SeqLanguage) (Dict: ResourceDictionary with Module R:=L.LP.R). +Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R). Export L. Export LP. @@ -115,7 +115,7 @@ Hint Rewrite set_spec_eq empty_spec: dict_rw. Fixpoint exp_tree (e: exp) (d old: deps): tree := match e with - | Name x => deps_get d x + | PReg x => deps_get d x | Op o le => Top o (list_exp_tree le d old) | Old e => exp_tree e old old end @@ -142,21 +142,21 @@ Proof. eauto. Qed. -Fixpoint macro_deps (i: macro) (d old: deps): deps := +Fixpoint inst_deps (i: inst) (d old: deps): deps := match i with | nil => d | (x, e)::i' => let t0:=deps_get d x in let t1:=exp_tree e d old in let v':=if failsafe t0 then t1 else (Terase t1 t0) in - macro_deps i' (Dict.set d x v') old + inst_deps i' (Dict.set d x v') old end. Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps := match p with | nil => d | i::p' => - let d':=macro_deps i d d in + let d':=inst_deps i d d in bblock_deps_rec p' d' end. @@ -177,9 +177,9 @@ Proof. - intros; erewrite IHe, IHe0; eauto. Qed. -Lemma tree_eval_macro_abort i m0 x old: forall d, +Lemma tree_eval_inst_abort i m0 x old: forall d, tree_eval (deps_get d x) m0 = None -> - tree_eval (deps_get (macro_deps i d old) x) m0 = None. + tree_eval (deps_get (inst_deps i d old) x) m0 = None. Proof. induction i as [|[y e] i IHi]; simpl; auto. intros d H; erewrite IHi; eauto. clear IHi. @@ -197,15 +197,15 @@ Lemma tree_eval_abort p m0 x: forall d, Proof. induction p; simpl; auto. intros d H; erewrite IHp; eauto. clear IHp. - eapply tree_eval_macro_abort; eauto. + eapply tree_eval_inst_abort; eauto. Qed. -Lemma tree_eval_macro_Some_correct1 i m0 old od: +Lemma tree_eval_inst_Some_correct1 i m0 old od: (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> forall (m1 m2: mem) d, - macro_run ge i m1 old = Some m2 -> + inst_run ge i m1 old = Some m2 -> (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)). + (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)). Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. @@ -222,7 +222,7 @@ Proof. + inversion H. Qed. -Local Hint Resolve tree_eval_macro_Some_correct1 tree_eval_abort. +Local Hint Resolve tree_eval_inst_Some_correct1 tree_eval_abort. Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, run ge p m1 = Some m2 -> @@ -232,7 +232,7 @@ Proof. induction p as [ | i p]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (macro_run ge i m1 m1) as om. + remember (inst_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _ _ _ _); eauto. + inversion H. @@ -246,10 +246,10 @@ Proof. intros; autorewrite with dict_rw; simpl; eauto. Qed. -Lemma tree_eval_macro_None_correct i m0 old od: +Lemma tree_eval_inst_None_correct i m0 old od: (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> forall m1 d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - macro_run ge i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None. + inst_run ge i m1 old = None <-> exists x, tree_eval (deps_get (inst_deps i d od) x) m0 = None. Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. @@ -264,7 +264,7 @@ Proof. * rewrite set_spec_diff; auto. + intuition. constructor 1 with (x:=x); simpl. - apply tree_eval_macro_abort. + apply tree_eval_inst_abort. autorewrite with dict_rw. destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. @@ -278,12 +278,12 @@ Proof. induction p as [|i p IHp]; simpl; intros m1 d. - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. - intros H0. - remember (macro_run ge i m1 m1) as om. + remember (inst_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _); eauto. + intuition. - assert (X: macro_run ge i m1 m1 = None); auto. - rewrite tree_eval_macro_None_correct in X; auto. + assert (X: inst_run ge i m1 m1 = None); auto. + rewrite tree_eval_inst_None_correct in X; auto. destruct X as [x H1]. constructor 1 with (x:=x); simpl; auto. Qed. @@ -295,12 +295,12 @@ Proof. intros; autorewrite with dict_rw; simpl; eauto. Qed. -Lemma tree_eval_macro_Some_correct2 i m0 old od: +Lemma tree_eval_inst_Some_correct2 i m0 old od: (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> forall (m1 m2: mem) d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)) -> - res_eq (Some m2) (macro_run ge i m1 old). + (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)) -> + res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0. @@ -317,7 +317,7 @@ Proof. erewrite tree_eval_exp; eauto. * rewrite set_spec_diff; auto. + generalize (H x). - rewrite tree_eval_macro_abort; try discriminate. + rewrite tree_eval_inst_abort; try discriminate. autorewrite with dict_rw. destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. @@ -333,11 +333,11 @@ Proof. generalize (H0 x); rewrite H. congruence. - intros H. - remember (macro_run ge i m1 m1) as om. + remember (inst_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _ _ _); eauto. - + assert (X: macro_run ge i m1 m1 = None); auto. - rewrite tree_eval_macro_None_correct in X; auto. + + assert (X: inst_run ge i m1 m1 = None); auto. + rewrite tree_eval_inst_None_correct in X; auto. destruct X as [x H1]. generalize (H x). rewrite tree_eval_abort; congruence. @@ -377,7 +377,7 @@ End DepTree. Require Import PArith. Require Import FMapPositive. -Module PosDict <: ResourceDictionary with Module R:=Pos. +Module PosDict <: PseudoRegDictionary with Module R:=Pos. Module R:=Pos. diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 9051f6ad..a4dd12eb 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -42,7 +42,7 @@ End ISeqLanguage. Module Type ImpDict. -Include ResourceDictionary. +Include PseudoRegDictionary. Parameter eq_test: forall {A}, t A -> t A -> ?? bool. @@ -171,7 +171,7 @@ Hint Resolve hdeps_get_correct: wlp. Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree := match e with - | Name x => hdeps_get d x dbg + | PReg x => hdeps_get d x dbg | Op o le => DO lt <~ hlist_exp_tree le d od;; hTop o lt dbg @@ -209,7 +209,7 @@ Hint Resolve hexp_tree_correct: wlp. Variable debug_assign: R.t -> ?? option pstring. -Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps := +Fixpoint hinst_deps (i: inst) (d od: hdeps): ?? hdeps := match i with | nil => RET d | (x, e)::i' => @@ -221,7 +221,7 @@ Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps := else DO t1 <~ hexp_tree e d od None;; hTerase t1 t0 dbg);; - hmacro_deps i' (Dict.set d x v') od + hinst_deps i' (Dict.set d x v') od end. Lemma pset_spec_eq d x t: @@ -244,11 +244,11 @@ Qed. Hint Rewrite pset_spec_eq pempty_spec: dict_rw. -Lemma hmacro_deps_correct i: forall d1 od1, - WHEN hmacro_deps i d1 od1 ~> d1' THEN +Lemma hinst_deps_correct i: forall d1 od1, + WHEN hinst_deps i d1 od1 ~> d1' THEN forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) -> (forall x, pdeps_get d1 x = deps_get d2 x) -> - forall x, pdeps_get d1' x = deps_get (macro_deps i d2 od2) x. + forall x, pdeps_get d1' x = deps_get (inst_deps i d2 od2) x. Proof. induction i; simpl; wlp_simplify. + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). @@ -265,10 +265,10 @@ Proof. * rewrite set_spec_diff, pset_spec_diff; auto. - rewrite H, H5; auto. Qed. -Global Opaque hmacro_deps. -Hint Resolve hmacro_deps_correct: wlp. +Global Opaque hinst_deps. +Hint Resolve hinst_deps_correct: wlp. -(* logging info: we log the number of macro-instructions passed ! *) +(* logging info: we log the number of inst-instructions passed ! *) Variable log: unit -> ?? unit. Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := @@ -276,7 +276,7 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := | nil => RET d | i::p' => log tt;; - DO d' <~ hmacro_deps i d d;; + DO d' <~ hinst_deps i d d;; hbblock_deps_rec p' d' end. @@ -371,10 +371,10 @@ Local Hint Resolve hbblock_deps_correct Dict.eq_test_correct: wlp. Section Prog_Eq_Gen. -Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 macros *) -Variable dbg2: R.t -> ?? option pstring. (* log of p2 macros *) -Variable log1: unit -> ?? unit. (* log of p1 macros *) -Variable log2: unit -> ?? unit. (* log of p2 macros *) +Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 insts *) +Variable dbg2: R.t -> ?? option pstring. (* log of p2 insts *) +Variable log1: unit -> ?? unit. (* log of p1 insts *) +Variable log2: unit -> ?? unit. (* log of p2 insts *) Variable hco_tree: hashConsing tree. diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 6eb0c5af..9745e35c 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -132,6 +132,7 @@ Proof. destruct x; simpl; auto. Qed. + (* Tactics MAIN tactics: @@ -184,4 +185,11 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). + +(* impure lazy andb of booleans *) +Definition iandb (k1 k2: ??bool): ?? bool := + DO r1 <~ k1 ;; + if r1 then k2 else RET false. + +Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index e7c7a9fb..8d904be6 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -77,14 +77,14 @@ Qed. End PhysEqModel. - Export PhysEqModel. Extract Constant phys_eq => "(==)". Hint Resolve phys_eq_correct: wlp. + Axiom struct_eq: forall {A}, A -> A -> ?? bool. -Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN b=true -> x=y. +Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y. Extract Constant struct_eq => "(=)". Hint Resolve struct_eq_correct: wlp. diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index 065c0922..d1971e57 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -21,20 +21,20 @@ Local Open Scope list. Section PARALLEL. Variable ge: genv. -(* parallel run of a macro *) -Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem := +(* parallel run of a inst *) +Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem := match i with | nil => Some m | (x, e)::i' => match exp_eval ge e tmp old with - | Some v' => macro_prun i' (assign m x v') (assign tmp x v') old + | Some v' => inst_prun i' (assign m x v') (assign tmp x v') old | None => None end end. -(* [macro_prun] is generalization of [macro_run] *) -Lemma macro_run_prun i: forall m old, - macro_run ge i m old = macro_prun i m m old. +(* [inst_prun] is generalization of [inst_run] *) +Lemma inst_run_prun i: forall m old, + inst_run ge i m old = inst_prun i m m old. Proof. induction i as [|[y e] i']; simpl; auto. intros m old; destruct (exp_eval ge e m old); simpl; auto. @@ -46,7 +46,7 @@ Fixpoint prun_iw (p: bblock) m old: option mem := match p with | nil => Some m | i::p' => - match macro_prun i m old old with + match inst_prun i m old old with | Some m1 => prun_iw p' m1 old | None => None end @@ -58,9 +58,9 @@ Definition prun (p: bblock) m (om: option mem) := exists p', res_eq om (prun_iw (* a few lemma on equality *) -Lemma macro_prun_equiv i old: forall m1 m2 tmp, +Lemma inst_prun_equiv i old: forall m1 m2 tmp, (forall x, m1 x = m2 x) -> - res_eq (macro_prun i m1 tmp old) (macro_prun i m2 tmp old). + res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old). Proof. induction i as [|[x e] i']; simpl; eauto. intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto. @@ -73,37 +73,43 @@ Lemma prun_iw_equiv p: forall m1 m2 old, Proof. induction p as [|i p']; simpl; eauto. - intros m1 m2 old H. - generalize (macro_prun_equiv i old m1 m2 old H); - destruct (macro_prun i m1 old old); simpl. + generalize (inst_prun_equiv i old m1 m2 old H); + destruct (inst_prun i m1 old old); simpl. + intros (m3 & H3 & H4); rewrite H3; simpl; eauto. + intros H1; rewrite H1; simpl; auto. Qed. + +Lemma prun_iw_app p1: forall m1 old p2, + prun_iw (p1++p2) m1 old = + match prun_iw p1 m1 old with + | Some m2 => prun_iw p2 m2 old + | None => None + end. +Proof. + induction p1; simpl; try congruence. + intros; destruct (inst_prun _ _ _); simpl; auto. +Qed. + Lemma prun_iw_app_None p1: forall m1 old p2, prun_iw p1 m1 old = None -> prun_iw (p1++p2) m1 old = None. Proof. - induction p1; simpl; try congruence. - intros; destruct (macro_prun _ _ _); simpl; auto. + intros m1 old p2 H; rewrite prun_iw_app. rewrite H; auto. Qed. Lemma prun_iw_app_Some p1: forall m1 old m2 p2, prun_iw p1 m1 old = Some m2 -> prun_iw (p1++p2) m1 old = prun_iw p2 m2 old. Proof. - induction p1; simpl; try congruence. - intros; destruct (macro_prun _ _ _); simpl; auto. - congruence. + intros m1 old m2 p2 H; rewrite prun_iw_app. rewrite H; auto. Qed. - End PARALLEL. End ParallelSemantics. - - Fixpoint notIn {A} (x: A) (l:list A): Prop := match l with | nil => True @@ -266,15 +272,15 @@ Qed. (** * Writing frames *) -Fixpoint macro_wframe(i:macro): list R.t := +Fixpoint inst_wframe(i:inst): list R.t := match i with | nil => nil - | a::i' => (fst a)::(macro_wframe i') + | a::i' => (fst a)::(inst_wframe i') end. -Lemma macro_wframe_correct i m' old: forall m tmp, - macro_prun ge i m tmp old = Some m' -> - forall x, notIn x (macro_wframe i) -> m' x = m x. +Lemma inst_wframe_correct i m' old: forall m tmp, + inst_prun ge i m tmp old = Some m' -> + forall x, notIn x (inst_wframe i) -> m' x = m x. Proof. induction i as [|[y e] i']; simpl. - intros m tmp H x H0; inversion_clear H; auto. @@ -283,47 +289,47 @@ Proof. rewrite assign_diff; auto. Qed. -Lemma macro_prun_fequiv i old: forall m1 m2 tmp, - frame_eq (fun x => In x (macro_wframe i)) (macro_prun ge i m1 tmp old) (macro_prun ge i m2 tmp old). +Lemma inst_prun_fequiv i old: forall m1 m2 tmp, + frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old). Proof. induction i as [|[y e] i']; simpl. - intros m1 m2 tmp; eexists; intuition eauto. - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto. eapply frame_eq_list_split; eauto. clear IHi'. intros m1' m2' x H1 H2. - lapply (macro_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto. - lapply (macro_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto. + lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto. + lapply (inst_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto. intros Xm2 Xm1 H H0. destruct H. + subst. rewrite Xm1, Xm2; auto. rewrite !assign_eq. auto. + rewrite <- notIn_iff in H0; tauto. Qed. -Lemma macro_prun_None i m1 m2 tmp old: - macro_prun ge i m1 tmp old = None -> - macro_prun ge i m2 tmp old = None. +Lemma inst_prun_None i m1 m2 tmp old: + inst_prun ge i m1 tmp old = None -> + inst_prun ge i m2 tmp old = None. Proof. - intros H; generalize (macro_prun_fequiv i old m1 m2 tmp). + intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). rewrite H; simpl; auto. Qed. -Lemma macro_prun_Some i m1 m2 tmp old m1': - macro_prun ge i m1 tmp old = Some m1' -> - res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun ge i m2 tmp old). +Lemma inst_prun_Some i m1 m2 tmp old m1': + inst_prun ge i m1 tmp old = Some m1' -> + res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old). Proof. - intros H; generalize (macro_prun_fequiv i old m1 m2 tmp). + intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). rewrite H; simpl. intros (m2' & H1 & H2). eexists; intuition eauto. rewrite frame_assign_def. - lapply (macro_wframe_correct i m2' old m2 tmp); eauto. - destruct (notIn_dec x (macro_wframe i)); auto. + lapply (inst_wframe_correct i m2' old m2 tmp); eauto. + destruct (notIn_dec x (inst_wframe i)); auto. intros X; rewrite X; auto. Qed. Fixpoint bblock_wframe(p:bblock): list R.t := match p with | nil => nil - | i::p' => (macro_wframe i)++(bblock_wframe p') + | i::p' => (inst_wframe i)++(bblock_wframe p') end. Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm. @@ -344,11 +350,11 @@ Proof. induction p as [|i p']; simpl. - intros m H; inversion_clear H; auto. - intros m H x; rewrite notIn_app; intros (H1 & H2). - remember (macro_prun i m old old) as om. + remember (inst_prun i m old old) as om. destruct om as [m1|]; simpl. + eapply eq_trans. eapply IHp'; eauto. - eapply macro_wframe_correct; eauto. + eapply inst_wframe_correct; eauto. + inversion H. Qed. @@ -357,13 +363,13 @@ Lemma prun_iw_fequiv p old: forall m1 m2, Proof. induction p as [|i p']; simpl. - intros m1 m2; eexists; intuition eauto. - - intros m1 m2; generalize (macro_prun_fequiv i old m1 m2 old). - remember (macro_prun i m1 old old) as om. + - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old). + remember (inst_prun i m1 old old) as om. destruct om as [m1'|]; simpl. + intros (m2' & H1 & H2). rewrite H1; simpl. eapply frame_eq_list_split; eauto. clear IHp'. intros m1'' m2'' x H3 H4. rewrite in_app_iff. - intros X X2. assert (X1: In x (macro_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. } + intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. } clear X. lapply (bblock_wframe_correct p' m1'' old m1'); eauto. lapply (bblock_wframe_correct p' m2'' old m2'); eauto. @@ -391,7 +397,7 @@ Fixpoint is_det (p: bblock): Prop := match p with | nil => True | i::p' => - disjoint (macro_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *) + disjoint (inst_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *) /\ is_det p' end. @@ -413,32 +419,32 @@ Theorem is_det_correct p p': Proof. induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto. - intros [H0 H1] m old. - remember (macro_prun ge i m old old) as om0. + remember (inst_prun ge i m old old) as om0. destruct om0 as [ m0 | ]; simpl; auto. - rewrite disjoint_app_r. intros ([Z1 Z2] & Z3 & Z4) m old. - remember (macro_prun ge i2 m old old) as om2. + remember (inst_prun ge i2 m old old) as om2. destruct om2 as [ m2 | ]; simpl; auto. - + remember (macro_prun ge i1 m old old) as om1. + + remember (inst_prun ge i1 m old old) as om1. destruct om1 as [ m1 | ]; simpl; auto. - * lapply (macro_prun_Some i2 m m1 old old m2); simpl; auto. - lapply (macro_prun_Some i1 m m2 old old m1); simpl; auto. + * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto. + lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto. intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2'). rewrite Hm1', Hm2'; simpl. eapply prun_iw_equiv. intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'. rewrite frame_assign_def. rewrite disjoint_sym in Z1; unfold disjoint in Z1. - destruct (notIn_dec x (macro_wframe i1)) as [ X1 | X1 ]. - { rewrite frame_assign_def; destruct (notIn_dec x (macro_wframe i2)) as [ X2 | X2 ]; auto. - erewrite (macro_wframe_correct i2 m2 old m old); eauto. - erewrite (macro_wframe_correct i1 m1 old m old); eauto. + destruct (notIn_dec x (inst_wframe i1)) as [ X1 | X1 ]. + { rewrite frame_assign_def; destruct (notIn_dec x (inst_wframe i2)) as [ X2 | X2 ]; auto. + erewrite (inst_wframe_correct i2 m2 old m old); eauto. + erewrite (inst_wframe_correct i1 m1 old m old); eauto. } rewrite frame_assign_notIn; auto. - * erewrite macro_prun_None; eauto. simpl; auto. - + remember (macro_prun ge i1 m old old) as om1. + * erewrite inst_prun_None; eauto. simpl; auto. + + remember (inst_prun ge i1 m old old) as om1. destruct om1 as [ m1 | ]; simpl; auto. - erewrite macro_prun_None; eauto. + erewrite inst_prun_None; eauto. - intros; eapply res_eq_trans. eapply IHPermutation1; eauto. eapply IHPermutation2; eauto. @@ -449,7 +455,7 @@ Qed. Fixpoint exp_frame (e: exp): list R.t := match e with - | Name x => x::nil + | PReg x => x::nil | Op o le => list_exp_frame le | Old e => exp_frame e end @@ -473,23 +479,23 @@ Proof. intros; (eapply H1 || eapply H2); rewrite in_app_iff; auto. Qed. -Fixpoint macro_frame (i: macro): list R.t := +Fixpoint inst_frame (i: inst): list R.t := match i with | nil => nil - | a::i' => (fst a)::(exp_frame (snd a) ++ macro_frame i') + | a::i' => (fst a)::(exp_frame (snd a) ++ inst_frame i') end. -Lemma macro_wframe_frame i x: In x (macro_wframe i) -> In x (macro_frame i). +Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i). Proof. induction i as [ | [y e] i']; simpl; intuition. Qed. -Lemma macro_frame_correct i wframe old1 old2: forall m tmp1 tmp2, - (disjoint (macro_frame i) wframe) -> +Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2, + (disjoint (inst_frame i) wframe) -> (forall x, notIn x wframe -> old1 x = old2 x) -> (forall x, notIn x wframe -> tmp1 x = tmp2 x) -> - macro_prun ge i m tmp1 old1 = macro_prun ge i m tmp2 old2. + inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2. Proof. induction i as [|[x e] i']; simpl; auto. intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l. @@ -509,8 +515,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop := match p with | nil => True | i::p' => - disjoint (macro_frame i) wframe (* no USE-AFTER-WRITE *) - /\ pararec p' ((macro_wframe i) ++ wframe) + disjoint (inst_frame i) wframe (* no USE-AFTER-WRITE *) + /\ pararec p' ((inst_wframe i) ++ wframe) end. Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe. @@ -521,7 +527,7 @@ Proof. generalize (IHp' _ H1). rewrite disjoint_app_r. intuition. eapply disjoint_incl_l. 2: eapply H0. - unfold incl. eapply macro_wframe_frame; eauto. + unfold incl. eapply inst_wframe_frame; eauto. Qed. Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p. @@ -540,13 +546,13 @@ Lemma pararec_correct p old: forall wframe m, Proof. elim p; clear p; simpl; auto. intros i p' X wframe m [H H0] H1. - erewrite macro_run_prun, macro_frame_correct; eauto. - remember (macro_prun ge i m old old) as om0. + erewrite inst_run_prun, inst_frame_correct; eauto. + remember (inst_prun ge i m old old) as om0. destruct om0 as [m0 | ]; try congruence. eapply X; eauto. intro x; rewrite notIn_app. intros [H3 H4]. rewrite <- H1; auto. - eapply macro_wframe_correct; eauto. + eapply inst_wframe_correct; eauto. Qed. Definition parallelizable (p: bblock) := pararec p nil. @@ -570,9 +576,9 @@ End PARALLELI. End ParallelizablityChecking. -Module Type ResourceSet. +Module Type PseudoRegSet. -Declare Module R: ResourceNames. +Declare Module R: PseudoRegisters. (** We assume a datatype [t] refining (list R.t) @@ -596,7 +602,7 @@ Parameter union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_fram Parameter is_disjoint: t -> t -> bool. Parameter is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. -End ResourceSet. +End PseudoRegSet. Lemma lazy_andb_bool_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true. @@ -607,7 +613,7 @@ Qed. -Module ParallelChecks (L: SeqLanguage) (S:ResourceSet with Module R:=L.LP.R). +Module ParallelChecks (L: SeqLanguage) (S:PseudoRegSet with Module R:=L.LP.R). Include ParallelizablityChecking L. @@ -618,20 +624,20 @@ Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.i (** Now, refinement of each operation toward parallelizable *) -Fixpoint macro_wsframe(i:macro): S.t := +Fixpoint inst_wsframe(i:inst): S.t := match i with | nil => S.empty - | a::i' => S.add (fst a) (macro_wsframe i') + | a::i' => S.add (fst a) (inst_wsframe i') end. -Lemma macro_wsframe_correct i: S.match_frame (macro_wsframe i) (macro_wframe i). +Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i). Proof. induction i; simpl; auto. Qed. Fixpoint exp_sframe (e: exp): S.t := match e with - | Name x => S.add x S.empty + | PReg x => S.add x S.empty | Op o le => list_exp_sframe le | Old e => exp_sframe e end @@ -647,27 +653,27 @@ Proof. induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto. Qed. -Fixpoint macro_sframe (i: macro): S.t := +Fixpoint inst_sframe (i: inst): S.t := match i with | nil => S.empty - | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (macro_sframe i')) + | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i')) end. Local Hint Resolve exp_sframe_correct. -Lemma macro_sframe_correct i: S.match_frame (macro_sframe i) (macro_frame i). +Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i). Proof. induction i as [|[y e] i']; simpl; auto. Qed. -Local Hint Resolve macro_wsframe_correct macro_sframe_correct. +Local Hint Resolve inst_wsframe_correct inst_sframe_correct. Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool := match p with | nil => true | i::p' => - S.is_disjoint (macro_sframe i) wsframe (* no USE-AFTER-WRITE *) - &&& is_pararec p' (S.union (macro_wsframe i) wsframe) + S.is_disjoint (inst_sframe i) wsframe (* no USE-AFTER-WRITE *) + &&& is_pararec p' (S.union (inst_wsframe i) wsframe) end. Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l). @@ -700,7 +706,7 @@ End ParallelChecks. Require Import PArith. Require Import MSets.MSetPositive. -Module PosResourceSet <: ResourceSet with Module R:=Pos. +Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos. Module R:=Pos. @@ -770,4 +776,4 @@ Proof. intros H4 H5; eapply is_disjoint_spec_true; eauto. Qed. -End PosResourceSet. +End PosPseudoRegSet. |