diff options
Diffstat (limited to 'mppa_k1c/abstractbb/DepExampleParallelTest.v')
| -rw-r--r-- | mppa_k1c/abstractbb/DepExampleParallelTest.v | 166 |
1 files changed, 0 insertions, 166 deletions
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 |