diff options
-rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 12 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepExampleDemo.v | 6 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepExampleEqTest.v | 24 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepExampleParallelTest.v | 13 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 55 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 46 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 64 |
7 files changed, 133 insertions, 87 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 50ce000e..21e7bd98 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -22,10 +22,12 @@ Parameter value: Type. Parameter op: Type. (* type of operations *) +Parameter genv: Type. (* environment to be used for evaluating an op *) + (* NB: possible generalization - relation after/before. *) -Parameter op_eval: op -> list value -> option value. +Parameter op_eval: genv -> op -> list value -> option value. End LangParam. @@ -38,6 +40,10 @@ Export P. Local Open Scope list. +Section SEQLANG. + +Variable ge: genv. + Definition mem := R.t -> value. Definition assign (m: mem) (x:R.t) (v: value): mem @@ -58,7 +64,7 @@ Fixpoint exp_eval (e: exp) (m old: mem): option value := | Name x => Some (m x) | Op o le => match list_exp_eval le m old with - | Some lv => op_eval o lv + | Some lv => op_eval ge o lv | _ => None end | Old e => exp_eval e old old @@ -201,6 +207,8 @@ Proof. eauto. Qed. +End SEQLANG. + End MkSeqLanguage. diff --git a/mppa_k1c/abstractbb/DepExampleDemo.v b/mppa_k1c/abstractbb/DepExampleDemo.v index c2079b70..74e8f35e 100644 --- a/mppa_k1c/abstractbb/DepExampleDemo.v +++ b/mppa_k1c/abstractbb/DepExampleDemo.v @@ -7,6 +7,10 @@ Open Scope Z_scope. Module EqTests. +Section TESTS. + +Variable ge: P.genv. + (**** TESTS DRIVER ! ****) Record test_input := { @@ -19,7 +23,7 @@ Record test_input := { Definition run1 (t: test_input): ?? unit := print ((name t) +; " =>");; - DO result <~ bblock_eq_test (verbose t) (p1 t) (p2 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" diff --git a/mppa_k1c/abstractbb/DepExampleEqTest.v b/mppa_k1c/abstractbb/DepExampleEqTest.v index 50bfc2f4..a633ee07 100644 --- a/mppa_k1c/abstractbb/DepExampleEqTest.v +++ b/mppa_k1c/abstractbb/DepExampleEqTest.v @@ -12,6 +12,10 @@ Module P<: ImpParam. Module R := Pos. +Definition genv := unit. + +Section IMP. + Inductive value_wrap := | Std (v:value) (* value = DepExample.value *) | Mem (m:mem) @@ -26,7 +30,7 @@ Inductive op_wrap := | STORE . -Definition op_eval (op: op_wrap) (l:list value_wrap): option value_wrap := +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)) @@ -47,7 +51,6 @@ Definition op_eval (op: op_wrap) (l:list value_wrap): option value_wrap := 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 @@ -63,6 +66,7 @@ Proof. destruct o1, o2; wlp_simplify; congruence. Qed. +End IMP. End P. @@ -77,6 +81,9 @@ 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. @@ -149,13 +156,13 @@ Definition match_option_state (os: option state) (om:option L.mem): Prop := | None => om = None end. -Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval (comp_op o) m old = Some (P.Std (operand_eval o (rm s))). +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 (comp_bblock p) m). +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. @@ -205,7 +212,7 @@ Proof. * rewrite L.assign_diff; auto. Qed. -Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run (comp_bblock p) (trans_state s)). +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. @@ -257,7 +264,7 @@ Proof. - intros; subst; simpl; auto. Qed. -Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2. +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. @@ -295,9 +302,9 @@ Definition string_of_op (op: P.op): ?? pstring := Definition bblock_eq_test (verb: bool) (p1 p2: bblock) : ?? bool := if verb then - IDT.verb_bblock_eq_test string_of_name string_of_op (comp_bblock p1) (comp_bblock p2) + IDT.verb_bblock_eq_test string_of_name string_of_op ge (comp_bblock p1) (comp_bblock p2) else - IDT.bblock_eq_test (comp_bblock p1) (comp_bblock p2). + 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. @@ -310,6 +317,7 @@ 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. diff --git a/mppa_k1c/abstractbb/DepExampleParallelTest.v b/mppa_k1c/abstractbb/DepExampleParallelTest.v index 00f33540..35b44683 100644 --- a/mppa_k1c/abstractbb/DepExampleParallelTest.v +++ b/mppa_k1c/abstractbb/DepExampleParallelTest.v @@ -8,13 +8,16 @@ Definition bblock_is_para (p: bblock) : bool := 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 (comp_bblock p) mout min). + 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. @@ -141,7 +144,7 @@ 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 (comp_bblock p) (trans_state s) (trans_option_state 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). @@ -154,8 +157,10 @@ 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 _ H); clear H. + intros H; generalize (PChk.is_parallelizable_correct ge _ H); clear H. intros H s os'. rewrite bblock_par_iff_prun, H. constructor; eauto. -Qed.
\ No newline at end of file +Qed. + +End SEC.
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index 3dff22e1..6f017378 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -41,6 +41,9 @@ Export L. Export LP. Local Open Scope list. +Section DEPTREE. + +Variable ge: genv. (** Dependency Trees of these "bblocks" @@ -63,7 +66,7 @@ Fixpoint tree_eval (t: tree) (m: mem): option value := | Tname x => Some (m x) | Top o l => match list_tree_eval l m with - | Some v => op_eval o v + | Some v => op_eval ge o v | _ => None end | Terase new old => @@ -127,7 +130,7 @@ Definition failsafe (t: tree): bool := match t with | Tname x => true | Top o Tnil => - match op_eval o nil with + match op_eval ge o nil with | Some _ => true | None => false end @@ -138,7 +141,7 @@ Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None. Proof. destruct t; simpl; try congruence. destruct l; simpl; try congruence. - destruct (op_eval o nil); try congruence. + destruct (op_eval ge o nil); try congruence. Qed. Fixpoint macro_deps (i: macro) (d old: deps): deps := @@ -168,10 +171,10 @@ Definition bblock_deps: bblock -> deps Lemma tree_eval_exp e od m0 old: (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (tree_eval (exp_tree e d od) m0) = exp_eval e m1 old. + (tree_eval (exp_tree e d od) m0) = exp_eval ge e m1 old. Proof. intro H. - induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval l m1 old); simpl; auto. + induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); simpl; auto. - intros; erewrite IHe; eauto. - intros; erewrite IHe, IHe0; eauto. Qed. @@ -202,14 +205,14 @@ Qed. Lemma tree_eval_macro_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 i m1 old = Some m2 -> + macro_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)). Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (exp_eval e m1 old) as ov. + remember (exp_eval ge e m1 old) as ov. destruct ov. + refine (IHi _ _ _ _ _ _); eauto. clear x0; intros x0. @@ -224,21 +227,21 @@ Qed. Local Hint Resolve tree_eval_macro_Some_correct1 tree_eval_abort. Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, - run p m1 = Some m2 -> + run ge p m1 = Some m2 -> (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)). Proof. induction p as [ | i p]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (macro_run i m1 m1) as om. + remember (macro_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _ _ _ _); eauto. + inversion H. Qed. Lemma bblock_deps_Some_correct1 p m0 m1: - run p m0 = Some m1 + run ge p m0 = Some m1 -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x). Proof. intros; eapply tree_eval_Some_correct1; @@ -248,12 +251,12 @@ Qed. Lemma tree_eval_macro_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 i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None. + macro_run ge i m1 old = None <-> exists x, tree_eval (deps_get (macro_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]. - intros H0. - remember (exp_eval e m1 old) as ov. + remember (exp_eval ge e m1 old) as ov. destruct ov. + refine (IHi _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). @@ -272,23 +275,23 @@ Qed. Lemma tree_eval_None_correct p m0: forall m1 d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - run p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. + run ge p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. 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 i m1 m1) as om. + remember (macro_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _); eauto. + intuition. - assert (X: macro_run i m1 m1 = None); auto. + assert (X: macro_run ge i m1 m1 = None); auto. rewrite tree_eval_macro_None_correct in X; auto. destruct X as [x H1]. constructor 1 with (x:=x); simpl; auto. Qed. Lemma bblock_deps_None_correct p m: - run p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None. + run ge p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None. Proof. intros; eapply tree_eval_None_correct. intros; autorewrite with dict_rw; simpl; eauto. @@ -299,7 +302,7 @@ Lemma tree_eval_macro_Some_correct2 i m0 old od: 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 i m1 old). + res_eq (Some m2) (macro_run ge i m1 old). Proof. intro X. induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0. @@ -307,7 +310,7 @@ Proof. generalize (H0 x); rewrite H. congruence. - intros H. - remember (exp_eval e m1 old) as ov. + remember (exp_eval ge e m1 old) as ov. destruct ov. + refine (IHi _ _ _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). @@ -325,17 +328,17 @@ Qed. Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) -> - res_eq (Some m2) (run p m1). + res_eq (Some m2) (run ge p m1). Proof. induction p as [|i p]; simpl; intros m1 m2 d H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. - remember (macro_run i m1 m1) as om. + remember (macro_run ge i m1 m1) as om. destruct om. + refine (IHp _ _ _ _ _); eauto. - + assert (X: macro_run i m1 m1 = None); auto. + + assert (X: macro_run ge i m1 m1 = None); auto. rewrite tree_eval_macro_None_correct in X; auto. destruct X as [x H1]. generalize (H x). @@ -344,7 +347,7 @@ Qed. Lemma bblock_deps_Some_correct2 p m0 m1: (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x)) - -> res_eq (Some m1) (run p m0). + -> res_eq (Some m1) (run ge p m0). Proof. intros; eapply tree_eval_Some_correct2; eauto. intros; autorewrite with dict_rw; simpl; eauto. @@ -353,22 +356,24 @@ Qed. Theorem bblock_deps_equiv p1 p2: (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x) - -> bblock_equiv p1 p2. + -> bblock_equiv ge p1 p2. Proof. intros H m2. - remember (run p1 m2) as om1. + remember (run ge p1 m2) as om1. destruct om1; simpl. + apply bblock_deps_Some_correct2. intros; rewrite <- H. apply bblock_deps_Some_correct1; auto. + rewrite bblock_deps_None_correct. - assert (X: run p1 m2 = None); auto. + assert (X: run ge p1 m2 = None); auto. rewrite bblock_deps_None_correct in X. destruct X as [x Hx]. rewrite H in Hx. eauto. Qed. +End DEPTREE. + End DepTree. Require Import PArith. diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 65f12b8e..994c8e34 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -72,6 +72,8 @@ Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data Variable hC_list_tree: pre_hashV list_tree -> ?? hashV list_tree. Hypothesis hC_list_tree_correct: forall t, WHEN hC_list_tree t ~> t' THEN pre_data t=data t'. +Variable ge: genv. + (* First, we wrap constructors for hashed values !*) Local Open Scope positive. @@ -213,7 +215,7 @@ Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps := | (x, e)::i' => DO dbg <~ debug_assign x;; DO t0 <~ hdeps_get d x None;; - DO v' <~ (if failsafe (data t0) + DO v' <~ (if failsafe ge (data t0) then hexp_tree e d od dbg else @@ -246,20 +248,20 @@ Lemma hmacro_deps_correct i: forall d1 od1, WHEN hmacro_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 (macro_deps ge i d2 od2) x. Proof. induction i; simpl; wlp_simplify. - + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). + + cutrewrite (failsafe ge (deps_get d2 a0) = failsafe ge (data exta0)). - erewrite H0, H2; simpl; eauto. clear exta2 Hexta2 H2; auto. intros x0; destruct (R.eq_dec a0 x0). - * subst; autorewrite with dict_rw. erewrite H1; eauto. + * subst. autorewrite with dict_rw. rewrite set_spec_eq. erewrite H1; eauto. * rewrite set_spec_diff, pset_spec_diff; auto. - rewrite H, H4; auto. - + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). + + cutrewrite (failsafe ge (deps_get d2 a0) = failsafe ge (data exta0)). - erewrite H0, H3; simpl; eauto. clear exta3 Hexta3 H3; auto. intros x0; destruct (R.eq_dec a0 x0). * subst; autorewrite with dict_rw. rewrite H2. - erewrite H, H1; eauto. congruence. + erewrite H, H1; eauto. rewrite set_spec_eq. congruence. * rewrite set_spec_diff, pset_spec_diff; auto. - rewrite H, H5; auto. Qed. @@ -280,7 +282,7 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := Lemma hbblock_deps_rec_correct p: forall d1, WHEN hbblock_deps_rec p d1 ~> d1' THEN - forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec p d2) x. + forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec ge p d2) x. Proof. induction p; simpl; wlp_simplify. Qed. @@ -292,10 +294,10 @@ Definition hbblock_deps: bblock -> ?? hdeps := fun p => hbblock_deps_rec p Dict.empty. Lemma hbblock_deps_correct p: - WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x. + WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps ge p) x. Proof. unfold bblock_deps; wlp_simplify. erewrite H; eauto. - intros; autorewrite with dict_rw; auto. + intros; autorewrite with dict_rw; auto. rewrite empty_spec. reflexivity. Qed. Global Opaque hbblock_deps. @@ -373,7 +375,7 @@ 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 ge: genv. Variable hco_tree: hashConsing tree. @@ -386,8 +388,8 @@ Variable print_error: pstring -> ?? unit. Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := DO r <~ (TRY - DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;; - DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;; + DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) ge dbg1 log1 p1 ;; + DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) ge dbg2 log2 p2 ;; DO b <~ Dict.eq_test d1 d2 ;; if b then RET true else ( @@ -397,7 +399,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := CATCH_FAIL s, _ => print_error s;; RET false - ENSURE (fun b => b=true -> bblock_equiv p1 p2));; + ENSURE (fun b => b=true -> bblock_equiv ge p1 p2));; RET (`r). Obligation 1. destruct hco_tree_correct as [X1 X2], hco_list_correct as [Y1 Y2]. @@ -408,7 +410,7 @@ Obligation 1. Qed. Theorem g_bblock_eq_test_correct p1 p2: - WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2. + WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. Proof. wlp_simplify. destruct exta; simpl in * |- *; auto. @@ -437,11 +439,11 @@ Definition print_error (log: logger unit) (s:pstring): ?? unit println (msg_prefix +; msg_number +; n +; " -- " +; s). -Program Definition bblock_eq_test (p1 p2: bblock): ?? bool := +Program Definition bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := DO log <~ count_logger ();; DO hco_tree <~ mk_annot (hCons tree_hash_eq (fun _ => RET msg_unknow_tree));; DO hco_list <~ mk_annot (hCons list_tree_hash_eq (fun _ => RET msg_unknow_list_tree));; - g_bblock_eq_test no_dbg no_dbg skip (log_insert log) hco_tree _ hco_list _ print_error_end (print_error log) p1 p2. + g_bblock_eq_test no_dbg no_dbg skip (log_insert log) ge hco_tree _ hco_list _ print_error_end (print_error log) p1 p2. Obligation 1. generalize (hCons_correct _ _ _ _ H0); clear H0. constructor 1; wlp_simplify. @@ -453,8 +455,8 @@ Qed. Local Hint Resolve g_bblock_eq_test_correct. -Theorem bblock_eq_test_correct p1 p2: - WHEN bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2. +Theorem bblock_eq_test_correct ge p1 p2: + WHEN bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. Proof. wlp_simplify. Qed. @@ -688,7 +690,7 @@ Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing lis next_log hcl s ). -Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := +Program Definition verb_bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := DO log1 <~ count_logger ();; DO log2 <~ count_logger ();; DO cr <~ make_cref Nothing;; @@ -699,6 +701,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := simple_debug (hlog log1 hco_tree hco_list) (log_insert log2) + ge hco_tree _ hco_list _ (print_error_end1 hco_tree hco_list) @@ -717,6 +720,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := simple_debug (hlog log1 hco_tree hco_list) (log_insert log2) + ge hco_tree _ hco_list _ (print_error_end2 hco_tree hco_list) @@ -745,8 +749,8 @@ Obligation 4. constructor 1; wlp_simplify. Qed. -Theorem verb_bblock_eq_test_correct p1 p2: - WHEN verb_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2. +Theorem verb_bblock_eq_test_correct ge p1 p2: + WHEN verb_bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. Proof. wlp_simplify. Qed. diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index 6bfd8770..b6d1f142 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -18,12 +18,15 @@ Module ParallelSemantics (L: SeqLanguage). Export L. 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 := match i with | nil => Some m | (x, e)::i' => - match exp_eval e tmp old with + match exp_eval ge e tmp old with | Some v' => macro_prun i' (assign m x v') (assign tmp x v') old | None => None end @@ -31,10 +34,10 @@ Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem := (* [macro_prun] is generalization of [macro_run] *) Lemma macro_run_prun i: forall m old, - macro_run i m old = macro_prun i m m old. + macro_run ge i m old = macro_prun i m m old. Proof. induction i as [|[y e] i']; simpl; auto. - intros m old; destruct (exp_eval e m old); simpl; auto. + intros m old; destruct (exp_eval ge e m old); simpl; auto. Qed. @@ -60,7 +63,7 @@ Lemma macro_prun_equiv i old: forall m1 m2 tmp, res_eq (macro_prun i m1 tmp old) (macro_prun i m2 tmp old). Proof. induction i as [|[x e] i']; simpl; eauto. - intros m1 m2 tmp H; destruct (exp_eval e tmp old); simpl; auto. + intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto. eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto. Qed. @@ -76,6 +79,7 @@ Proof. + intros H1; rewrite H1; simpl; auto. Qed. +End PARALLEL. End ParallelSemantics. @@ -168,6 +172,8 @@ Module ParallelizablityChecking (L: SeqLanguage). Include ParallelSemantics L. +Section PARALLELI. +Variable ge: genv. (** * Preliminary notions on frames *) @@ -249,22 +255,22 @@ Fixpoint macro_wframe(i:macro): list R.t := end. Lemma macro_wframe_correct i m' old: forall m tmp, - macro_prun i m tmp old = Some m' -> + macro_prun ge i m tmp old = Some m' -> forall x, notIn x (macro_wframe i) -> m' x = m x. Proof. induction i as [|[y e] i']; simpl. - intros m tmp H x H0; inversion_clear H; auto. - - intros m tmp H x (H1 & H2); destruct (exp_eval e tmp old); simpl; try congruence. + - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence. cutrewrite (m x = assign m y v x); eauto. 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 i m1 tmp old) (macro_prun i m2 tmp old). + frame_eq (fun x => In x (macro_wframe i)) (macro_prun ge i m1 tmp old) (macro_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 e tmp old); simpl; auto. + - 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. @@ -275,16 +281,16 @@ Proof. Qed. Lemma macro_prun_None i m1 m2 tmp old: - macro_prun i m1 tmp old = None -> - macro_prun i m2 tmp old = None. + macro_prun ge i m1 tmp old = None -> + macro_prun ge i m2 tmp old = None. Proof. intros H; generalize (macro_prun_fequiv i old m1 m2 tmp). rewrite H; simpl; auto. Qed. Lemma macro_prun_Some i m1 m2 tmp old m1': - macro_prun i m1 tmp old = Some m1' -> - res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun i m2 tmp old). + 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). Proof. intros H; generalize (macro_prun_fequiv i old m1 m2 tmp). rewrite H; simpl. @@ -385,17 +391,17 @@ Qed. Theorem is_det_correct p p': Permutation p p' -> is_det p -> - forall m old, res_eq (prun_iw p m old) (prun_iw p' m old). + forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old). Proof. induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto. - intros [H0 H1] m old. - remember (macro_prun i m old old) as om0. + remember (macro_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 i2 m old old) as om2. + remember (macro_prun ge i2 m old old) as om2. destruct om2 as [ m2 | ]; simpl; auto. - + remember (macro_prun i1 m old old) as om1. + + remember (macro_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. @@ -412,7 +418,7 @@ Proof. } rewrite frame_assign_notIn; auto. * erewrite macro_prun_None; eauto. simpl; auto. - + remember (macro_prun i1 m old old) as om1. + + remember (macro_prun ge i1 m old old) as om1. destruct om1 as [ m1 | ]; simpl; auto. erewrite macro_prun_None; eauto. - intros; eapply res_eq_trans. @@ -439,10 +445,10 @@ with list_exp_frame (le: list_exp): list R.t := Lemma exp_frame_correct e old1 old2: (forall x, In x (exp_frame e) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (exp_frame e) -> m1 x = m2 x) -> - (exp_eval e m1 old1)=(exp_eval e m2 old2). + (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2). Proof. induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) -> - (list_exp_eval l m1 old1)=(list_exp_eval l m2 old2)); simpl; auto. + (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; auto. - intros H1 m1 m2 H2; rewrite H2; auto. - intros H1 m1 m2 H2; erewrite IHe; eauto. - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; @@ -465,13 +471,13 @@ Lemma macro_frame_correct i wframe old1 old2: forall m tmp1 tmp2, (disjoint (macro_frame i) wframe) -> (forall x, notIn x wframe -> old1 x = old2 x) -> (forall x, notIn x wframe -> tmp1 x = tmp2 x) -> - macro_prun i m tmp1 old1 = macro_prun i m tmp2 old2. + macro_prun ge i m tmp1 old1 = macro_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. intros (H1 & H2 & H3) H6 H7. - cutrewrite (exp_eval e tmp1 old1 = exp_eval e tmp2 old2). - - destruct (exp_eval e tmp2 old2); auto. + cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2). + - destruct (exp_eval ge e tmp2 old2); auto. eapply IHi'; eauto. simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. - unfold disjoint in H2; apply exp_frame_correct. @@ -512,12 +518,12 @@ Qed. Lemma pararec_correct p old: forall wframe m, pararec p wframe -> (forall x, notIn x wframe -> m x = old x) -> - run p m = prun_iw p m old. + run ge p m = prun_iw ge p m old. 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 i m old old) as om0. + remember (macro_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]. @@ -528,7 +534,7 @@ Qed. Definition parallelizable (p: bblock) := pararec p nil. Theorem parallelizable_correct p m om': - parallelizable p -> (prun p m om' <-> res_eq om' (run p m)). + parallelizable p -> (prun ge p m om' <-> res_eq om' (run ge p m)). Proof. intros H. constructor 1. - intros (p' & H0 & H1). eapply res_eq_trans; eauto. @@ -541,6 +547,8 @@ Proof. erewrite pararec_correct in H0; eauto. Qed. +End PARALLELI. + End ParallelizablityChecking. @@ -585,6 +593,9 @@ Module ParallelChecks (L: SeqLanguage) (S:ResourceSet with Module R:=L.LP.R). Include ParallelizablityChecking L. +Section PARALLEL2. +Variable ge: genv. + Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame. (** Now, refinement of each operation toward parallelizable *) @@ -656,12 +667,13 @@ Proof. Qed. Theorem is_parallelizable_correct p: - is_parallelizable p = true -> forall m om', (prun p m om' <-> res_eq om' (run p m)). + is_parallelizable p = true -> forall m om', (prun ge p m om' <-> res_eq om' (run ge p m)). Proof. intros; apply parallelizable_correct. apply is_para_correct_aux. auto. Qed. +End PARALLEL2. End ParallelChecks. |