From af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 22 Mar 2019 15:44:38 +0100 Subject: Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu_par MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblockdeps.v | 68 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 68 insertions(+) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c6052337..0c6c74fb 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1459,3 +1459,71 @@ Module PChk := ParallelChecks L PosResourceSet. Definition bblock_para_check (p: Asmblock.bblock) : bool := PChk.is_parallelizable (trans_block p). + +Require Import Asmvliw. +Import PChk. + +Section SECT. +Variable Ge: genv. + +Theorem forward_simu_par: + forall rs1 m1 s1' b ge fn rs2 m2, + Ge = Genv ge fn -> + parexec_bblock ge fn b rs1 m1 (Next rs2 m2) -> + match_states (State rs1 m1) s1' -> + exists s2', + prun Ge (trans_block b) s1' (Some s2') + /\ match_states (State rs2 m2) s2'. +Proof. +Admitted. + +Theorem forward_simu_par_stuck: + forall rs1 m1 s1' b ge fn, + Ge = Genv ge fn -> + parexec_bblock ge fn b rs1 m1 Stuck -> + match_states (State rs1 m1) s1' -> + prun Ge (trans_block b) s1' None. +Proof. +Admitted. + +Theorem forward_simu_par_alt: + forall rs1 m1 s1' b ge fn o2, + Ge = Genv ge fn -> + match_states (State rs1 m1) s1' -> + parexec_bblock ge fn b rs1 m1 o2 -> + exists o2', + prun Ge (trans_block b) s1' o2' + /\ match_outcome o2 o2'. +Proof. + intros until o2. intros GENV MS PAREXEC. destruct o2 eqn:O2. + - exploit forward_simu_par; eauto. intros (s2' & PRUN & MS'). eexists. split. eassumption. + unfold match_outcome. eexists; split; auto. + - exploit forward_simu_par_stuck; eauto. intros. eexists; split; eauto. + constructor; auto. +Qed. + +Lemma bblock_para_check_correct: + forall ge fn bb rs m rs' m' o, + Ge = Genv ge fn -> + exec_bblock ge fn bb rs m = Next rs' m' -> + bblock_para_check bb = true -> + parexec_bblock ge fn bb rs m o -> + o = Next rs' m'. +Proof. + intros. unfold bblock_para_check in H1. + exploit forward_simu; eauto. eapply trans_state_match. + intros (s2' & EXEC & MS). + exploit forward_simu_par_alt. 2: apply (trans_state_match (State rs m)). all: eauto. + intros (o2' & PRUN & MO). + exploit parallelizable_correct. apply is_para_correct_aux. eassumption. + intro. eapply H3 in PRUN. clear H3. destruct o2'. + - inv PRUN. inv H3. unfold exec in EXEC. assert (x = s2') by congruence. subst. clear H. + assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4. + destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst. + exploit state_equiv. split. eapply MS. eapply H4. intros. inv H. reflexivity. + - unfold match_outcome in MO. destruct o. + + inv MO. inv H3. discriminate. + + clear MO. unfold exec in EXEC. rewrite EXEC in PRUN. discriminate. +Qed. + +End SECT. -- cgit From 990dae34a6f132b3f7a3be438d47555805831085 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 22 Mar 2019 16:03:00 +0100 Subject: fix for Coq.8.8 ?? --- mppa_k1c/Asmblockdeps.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 0c6c74fb..35138123 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1463,7 +1463,8 @@ Definition bblock_para_check (p: Asmblock.bblock) : bool := Require Import Asmvliw. Import PChk. -Section SECT. +Section SECT_PAR. + Variable Ge: genv. Theorem forward_simu_par: @@ -1526,4 +1527,4 @@ Proof. + clear MO. unfold exec in EXEC. rewrite EXEC in PRUN. discriminate. Qed. -End SECT. +End SECT_PAR. -- cgit From 62505aeb0303126cac8f1e3f8fb06414c9cd4fb0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 22 Mar 2019 17:13:06 +0100 Subject: Avancement dans la preuve des bundles --- mppa_k1c/Asmblockdeps.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 51 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 35138123..a2941b6d 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1460,13 +1460,48 @@ Module PChk := ParallelChecks L PosResourceSet. Definition bblock_para_check (p: Asmblock.bblock) : bool := PChk.is_parallelizable (trans_block p). -Require Import Asmvliw. +Require Import Asmvliw Permutation. Import PChk. Section SECT_PAR. Variable Ge: genv. +Theorem forward_simu_par_wio: + forall ge fn rs1 m1 s1' bdy1 bdy2 b rs m rs2 m2 rs3 m3, + Ge = Genv ge fn -> + match_states (State rs m) s1' -> + Permutation (bdy1 ++ bdy2) (body b) -> + parexec_wio_body ge bdy1 rs rs m m = Next rs1 m1 -> + parexec_control ge fn (exit b) rs (par_nextblock (Ptrofs.repr (size b)) rs rs1) m1 = Next rs2 m2 -> + parexec_wio_body ge bdy2 rs rs2 m m2 = Next rs3 m3 -> + exists s2', + res_eq (Some s2') (prun_iw Ge (trans_block b) s1' s1') + /\ match_states (State rs3 m3) s2'. +Proof. +Admitted. + +Lemma forward_simu_par_wio_stuck_bdy1: + forall ge fn rs m s1' bdy1 bdy2 b, + Ge = Genv ge fn -> + match_states (State rs m) s1' -> + Permutation (bdy1 ++ bdy2) (body b) -> + parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> + res_eq None (prun_iw Ge (trans_block b) s1' s1'). +Proof. +Admitted. + +Lemma forward_simu_par_wio_stuck_bdy2: + forall ge fn rs m s1' bdy1 bdy2 b m' rs', + Ge = Genv ge fn -> + match_states (State rs m) s1' -> + Permutation (bdy1 ++ bdy2) (body b) -> + parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rs' m' -> + parexec_wio_body ge bdy2 rs rs' m m' = Stuck -> + res_eq None (prun_iw Ge (trans_block b) s1' s1'). +Proof. +Admitted. + Theorem forward_simu_par: forall rs1 m1 s1' b ge fn rs2 m2, Ge = Genv ge fn -> @@ -1476,7 +1511,15 @@ Theorem forward_simu_par: prun Ge (trans_block b) s1' (Some s2') /\ match_states (State rs2 m2) s2'. Proof. -Admitted. + intros until m2. intros GENV PAREXEC MS. + inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). + destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT; try discriminate. + unfold parexec_wio_bblock_aux in WIOEXIT. destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOBODY; try discriminate. + exploit forward_simu_par_wio; eauto. intros (s2' & PIW & MS'). + eexists. split. + econstructor; eauto. + eassumption. +Qed. Theorem forward_simu_par_stuck: forall rs1 m1 s1' b ge fn, @@ -1485,7 +1528,12 @@ Theorem forward_simu_par_stuck: match_states (State rs1 m1) s1' -> prun Ge (trans_block b) s1' None. Proof. -Admitted. + intros until fn. intros GENV PAREXEC MS. + inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). + destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT. + - econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy2; eauto. auto. + - clear WIO. econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy1; eauto. auto. +Qed. Theorem forward_simu_par_alt: forall rs1 m1 s1' b ge fn o2, -- cgit From 38797928d764b838194dbc685643ef9eb13603da Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 26 Mar 2019 16:32:14 +0100 Subject: Un peu d'avancement --- mppa_k1c/Asmblockdeps.v | 276 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 274 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a2941b6d..6417055a 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1465,8 +1465,281 @@ Import PChk. Section SECT_PAR. +Ltac Simplif := + ((rewrite nextblock_inv by eauto with asmgen) + || (rewrite nextblock_inv1 by eauto with asmgen) + || (rewrite Pregmap.gss) + || (rewrite nextblock_pc) + || (rewrite Pregmap.gso by eauto with asmgen) + || (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); + try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto)) + || (rewrite assign_eq) + ); auto with asmgen. + +Ltac Simpl := repeat Simplif. + +Arguments Pos.add: simpl never. +Arguments ppos: simpl never. + Variable Ge: genv. +Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' mw' i: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_arith_instr ge i rsr rsw = rsw' -> mw = mw' -> + exists sw', + macro_prun Ge (trans_arith i) sw sr sr = Some sw' + /\ match_states (State rsw' mw') sw'. +Proof. + intros GENV MSR MSW PARARITH MWEQ. subst. inv MSR. inv MSW. + unfold parexec_arith_instr. destruct i. +(* Ploadsymbol *) + - destruct i. eexists; split; [| split]. + * simpl. reflexivity. + * Simpl. + * simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRR *) + - eexists; split; [| split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRI32 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRI64 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF32 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF64 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRR *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRI32 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRI64 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +Qed. + +Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi rsw' mw': + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_basic_instr ge bi rsr rsw mr mw = Next rsw' mw' -> + exists sw', + macro_prun Ge (trans_basic bi) sw sr sr = Some sw' + /\ match_states (State rsw' mw') sw'. +Proof. + intros GENV MSR MSW H. + destruct bi. +(* Arith *) + - simpl in H. inversion H. subst rsw' mw'. simpl macro_prun. eapply trans_arith_par_correct; eauto. +(* Load *) + - simpl in H. destruct i. + unfold parexec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; + destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H. inv MSR; inv MSW; + eexists; split; try split; + [ simpl; rewrite EVALOFF; rewrite H; pose (H0 ra); simpl in e; rewrite e; rewrite MEML; reflexivity| + Simpl| + intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); [ + subst; Simpl| + Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]]. +(* Store *) + - simpl in H. destruct i. + unfold parexec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate. + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate. inv H; inv MSR; inv MSW. + eexists; split; try split. + * simpl. rewrite EVALOFF. rewrite H. rewrite (H0 ra). rewrite (H0 rs). rewrite MEML. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. +(* Allocframe *) + - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. + inv H. inv MSR. inv MSW. eexists. split; try split. + * simpl. Simpl. rewrite (H0 GPR12). rewrite H. rewrite MEMAL. rewrite MEMS. Simpl. + rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl. +(* Freeframe *) + - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rsr GPR12) eqn:SPeq; try discriminate. + destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv MSR. inv MSW. + eexists. split; try split. + * simpl. rewrite (H0 GPR12). rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE. + Simpl. rewrite (H0 GPR12). rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl. +(* Pget *) + - simpl in H. destruct rs eqn:rseq; try discriminate. inv H. inv MSR. inv MSW. + eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* Pset *) + - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv MSR; inv MSW. + eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. +(* Pnop *) + - simpl in H. inv H. inv MSR. inv MSW. eexists. split; try split. assumption. assumption. +Qed. + +Theorem forward_simu_par_body: + forall bdy ge fn rsr mr sr rsw mw sw rs' m', + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_wio_body ge bdy rsr rsw mr mw = Next rs' m' -> + exists s', + prun_iw Ge (trans_body bdy) sw sr = Some s' + /\ match_states (State rs' m') s'. +Proof. + induction bdy. + - intros until m'. intros GENV MSR MSW WIO. + simpl in WIO. inv WIO. inv MSR. inv MSW. + eexists. split; [| split]. + * simpl. reflexivity. + * assumption. + * assumption. + - intros until m'. intros GENV MSR MSW WIO. + simpl in WIO. destruct (parexec_basic_instr _ _ _ _ _ _) eqn:PARBASIC; try discriminate. + exploit forward_simu_par_wio_basic. 4: eapply PARBASIC. all: eauto. + intros (sw' & MPRUN & MS'). simpl prun_iw. rewrite MPRUN. + eapply IHbdy; eauto. +Qed. + +Theorem forward_simu_par_control ctl rsr mr sr rsw mw sw ge fn rs' m': + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_control ge fn (Some ctl) rsr rsw mw = Next rs' m' -> + exists s', + macro_prun Ge (trans_control ctl) sw sr sr = Some s' + /\ match_states (State rs' m') s'. +Proof. + intros GENV MSR MSW H0. + simpl in *. destruct ctl; destruct i; try discriminate. + all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [ simpl; reflexivity | Simpl | intros rr; destruct rr; Simpl]). + (* Pj_l *) + + unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. inv H0. + inv MSR; inv MSW. + eexists; split; try split. + * simpl. rewrite (H0 PC). unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + (* Pcb *) + + destruct (cmp_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. + ++ unfold par_eval_branch in H0. destruct (Val.cmp_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + ++ unfold par_eval_branch in H0. destruct (Val.cmpl_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0; inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + (* Pcbu *) + + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. + ++ unfold par_eval_branch in H0. destruct (Val_cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + ++ unfold par_eval_branch in H0. destruct (Val_cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0; inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. +Qed. + +Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> + exists s', + prun_iw Ge ((trans_body bdy) ++ trans_pcincr sz (trans_exit ex)) sr sw = Some s' + /\ match_states (State rs' m') s'. +Proof. + intros. unfold parexec_wio_bblock_aux in H2. + destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOB; try discriminate. + exploit forward_simu_par_body. 4: eapply WIOB. all: eauto. + intros (s' & RUNB & MS'). + destruct ex. + - exploit forward_simu_par_control. 4: eapply H2. all: eauto. +Admitted. + + Theorem forward_simu_par_wio: forall ge fn rs1 m1 s1' bdy1 bdy2 b rs m rs2 m2 rs3 m3, Ge = Genv ge fn -> @@ -1491,8 +1764,7 @@ Lemma forward_simu_par_wio_stuck_bdy1: Proof. Admitted. -Lemma forward_simu_par_wio_stuck_bdy2: - forall ge fn rs m s1' bdy1 bdy2 b m' rs', +Lemma forward_simu_par_wio_stuck_bdy2 ge fn rs m s1' bdy1 bdy2 b m' rs': Ge = Genv ge fn -> match_states (State rs m) s1' -> Permutation (bdy1 ++ bdy2) (body b) -> -- cgit From 8550881e22693a5cd5078980f3e9c23bf6f63424 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 26 Mar 2019 17:30:18 +0100 Subject: 1 coup de pouce ! --- mppa_k1c/Asmblockdeps.v | 38 +++++++++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 9 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 6417055a..4843b41d 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1722,16 +1722,18 @@ Proof. * intros rr; destruct rr; Simpl. Qed. -Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': +Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ trans_pcincr sz (trans_exit ex). + +Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> exists s', - prun_iw Ge ((trans_body bdy) ++ trans_pcincr sz (trans_exit ex)) sr sw = Some s' + prun_iw Ge (trans_block_aux bdy sz ex) sr sw = Some s' /\ match_states (State rs' m') s'. Proof. - intros. unfold parexec_wio_bblock_aux in H2. + intros. unfold parexec_wio_bblock_aux in H2. unfold trans_block_aux. destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOB; try discriminate. exploit forward_simu_par_body. 4: eapply WIOB. all: eauto. intros (s' & RUNB & MS'). @@ -1739,7 +1741,24 @@ Proof. - exploit forward_simu_par_control. 4: eapply H2. all: eauto. Admitted. +Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs' m' rs2 m2: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> + parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 -> + exists s2', + res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr) + /\ match_states (State rs2 m2) s2'. +Admitted. +Theorem trans_block_perserves_permutation ge fn bdy1 bdy2 b: + Ge = Genv ge fn -> + Permutation (bdy1 ++ bdy2) (body b) -> + Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). +Admitted. + +(* replaced by forward_simu_par_wio_bblock Theorem forward_simu_par_wio: forall ge fn rs1 m1 s1' bdy1 bdy2 b rs m rs2 m2 rs3 m3, Ge = Genv ge fn -> @@ -1753,6 +1772,7 @@ Theorem forward_simu_par_wio: /\ match_states (State rs3 m3) s2'. Proof. Admitted. +*) Lemma forward_simu_par_wio_stuck_bdy1: forall ge fn rs m s1' bdy1 bdy2 b, @@ -1785,12 +1805,12 @@ Theorem forward_simu_par: Proof. intros until m2. intros GENV PAREXEC MS. inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). - destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT; try discriminate. - unfold parexec_wio_bblock_aux in WIOEXIT. destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOBODY; try discriminate. - exploit forward_simu_par_wio; eauto. intros (s2' & PIW & MS'). - eexists. split. - econstructor; eauto. - eassumption. + exploit trans_block_perserves_permutation; eauto. + intros Perm. + remember (parexec_wio_bblock_aux _ _ _ _ _ _ _) as pwb. + destruct pwb; try congruence. + exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS'). + unfold prun; eexists; split; eauto. Qed. Theorem forward_simu_par_stuck: -- cgit From 25f47289ff5d9b497d45d3f4efbf4c5df56829a9 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 27 Mar 2019 16:25:40 +0100 Subject: Avancement dans Asmblockdeps.v --- mppa_k1c/Asmblockdeps.v | 197 +++++++++++++++++++++++++++--------------------- 1 file changed, 109 insertions(+), 88 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 4843b41d..df1acc6f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -555,10 +555,10 @@ Fixpoint trans_body (b: list basic) : list L.macro := | b :: lb => (trans_basic b) :: (trans_body lb) end. -Definition trans_pcincr (sz: Z) (k: L.macro) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k]. +Definition trans_pcincr (sz: Z) (k: L.macro) := (#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k. Definition trans_block (b: Asmblock.bblock) : L.bblock := - trans_body (body b) ++ trans_pcincr (size b) (trans_exit (exit b)). + trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil). Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. Proof. @@ -795,7 +795,7 @@ Lemma forward_simu_control: exec_control ge fn ex (nextblock b rs) m = Next rs2 m2 -> match_states (State rs m) s -> exists s', - exec Ge (trans_pcincr (size b) (trans_exit ex)) s = Some s' + exec Ge (trans_pcincr (size b) (trans_exit ex) :: nil) s = Some s' /\ match_states (State rs2 m2) s'. Proof. intros. destruct ex. @@ -972,7 +972,7 @@ Lemma exec_trans_pcincr_exec: forall rs m s b, match_states (State rs m) s -> exists s', - exec Ge (trans_pcincr (size b) (trans_exit (exit b))) s = exec Ge [trans_exit (exit b)] s' + exec Ge (trans_pcincr (size b) (trans_exit (exit b)) :: nil) s = exec Ge [trans_exit (exit b)] s' /\ match_states (State (nextblock b rs) m) s'. Proof. intros. @@ -1633,96 +1633,110 @@ Proof. eapply IHbdy; eauto. Qed. -Theorem forward_simu_par_control ctl rsr mr sr rsw mw sw ge fn rs' m': +Theorem forward_simu_par_control ge fn rsr rsw mr mw sr sw sz rs' ex m': Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_control ge fn (Some ctl) rsr rsw mw = Next rs' m' -> + parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Next rs' m' -> exists s', - macro_prun Ge (trans_control ctl) sw sr sr = Some s' + macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s' /\ match_states (State rs' m') s'. Proof. intros GENV MSR MSW H0. - simpl in *. destruct ctl; destruct i; try discriminate. - all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [ simpl; reflexivity | Simpl | intros rr; destruct rr; Simpl]). - (* Pj_l *) - + unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. inv H0. - inv MSR; inv MSW. - eexists; split; try split. - * simpl. rewrite (H0 PC). unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - (* Pcb *) - + destruct (cmp_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. - ++ unfold par_eval_branch in H0. destruct (Val.cmp_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. - inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - +++ inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - ++ unfold par_eval_branch in H0. destruct (Val.cmpl_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. - inv H0; inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - +++ inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. Simpl. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - (* Pcbu *) - + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. - ++ unfold par_eval_branch in H0. destruct (Val_cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. - inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - +++ inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - ++ unfold par_eval_branch in H0. destruct (Val_cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. - inv H0; inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - +++ inv H0. inv MSR; inv MSW. eexists; split; try split. - * simpl. rewrite (H0 PC). - rewrite CFB. Simpl. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. -Qed. + simpl in *. + destruct ex. + - destruct c; destruct i; try discriminate. + all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [simpl; rewrite (H0 PC); reflexivity | Simpl | intros rr; destruct rr; unfold par_nextblock; Simpl]). + + (* Pj_l *) + + simpl in H0. unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. inv H0. + inv MSR; inv MSW. + eexists; split; try split. + * simpl. rewrite (H0 PC). unfold goto_label_deps. rewrite LPOS. Simpl. + unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. + (* Pcb *) + + simpl in H0. destruct (cmp_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. + ++ unfold par_eval_branch in H0. destruct (Val.cmp_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. + inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. Admitted. (* rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + ++ unfold par_eval_branch in H0. destruct (Val.cmpl_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0; inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + (* Pcbu *) + + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. + ++ unfold par_eval_branch in H0. destruct (Val_cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + ++ unfold par_eval_branch in H0. destruct (Val_cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + inv H0; inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + +++ inv H0. inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. rewrite VALCMP. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. +Qed. *) +(* +Theorem forward_simu_par_nextblockge ge fn rsr rsw mr mw sr sw sz rs' ex rs'' m'': + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + par_nextblock (Ptrofs.repr sz) rsr rsw = rs' -> + parexec_control ge fn ex rsr rs' mw = Next rs'' m'' -> + exists s'', + macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'' + /\ match_states (State rs'' m'') s''. *) -Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ trans_pcincr sz (trans_exit ex). +Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': Ge = Genv ge fn -> @@ -1741,6 +1755,7 @@ Proof. - exploit forward_simu_par_control. 4: eapply H2. all: eauto. Admitted. + Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs' m' rs2 m2: Ge = Genv ge fn -> match_states (State rsr mr) sr -> @@ -1752,8 +1767,14 @@ Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs /\ match_states (State rs2 m2) s2'. Admitted. -Theorem trans_block_perserves_permutation ge fn bdy1 bdy2 b: - Ge = Genv ge fn -> +Lemma trans_body_perserves_permutation bdy1 bdy2: + Permutation bdy1 bdy2 -> + Permutation (trans_body bdy1) (trans_body bdy2). +Proof. + induction 1; simpl; econstructor; eauto. +Qed. + +Theorem trans_block_perserves_permutation bdy1 bdy2 b: Permutation (bdy1 ++ bdy2) (body b) -> Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). Admitted. -- cgit From 2a353a9380100279769d3a0f65a64b3114e3b11a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 27 Mar 2019 17:24:44 +0100 Subject: Preuve du forward_simu du parexec_wio_bblock_aux --- mppa_k1c/Asmblockdeps.v | 116 ++++++++++++++++++++++++++---------------------- 1 file changed, 63 insertions(+), 53 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index df1acc6f..a65be8a8 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1659,111 +1659,121 @@ Proof. (* Pcb *) + simpl in H0. destruct (cmp_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. ++ unfold par_eval_branch in H0. destruct (Val.cmp_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate. inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). rewrite CFB. Simpl. rewrite (H0 r). - unfold eval_branch_deps. Admitted. (* rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. + unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. +++ inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. ++ unfold par_eval_branch in H0. destruct (Val.cmpl_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate. inv H0; inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. + unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. +++ inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). rewrite CFB. Simpl. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. (* Pcbu *) - + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. + + simpl in H0. destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. ++ unfold par_eval_branch in H0. destruct (Val_cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate. inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. + unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. +++ inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. ++ unfold par_eval_branch in H0. destruct (Val_cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b. - +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate. + +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate. inv H0; inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). - rewrite CFB. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. - unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity. + rewrite CFB. Simpl. rewrite (H0 r). + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. + unfold goto_label_deps. rewrite LPOS. + unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. +++ inv H0. inv MSR; inv MSW. eexists; split; try split. * simpl. rewrite (H0 PC). rewrite CFB. Simpl. rewrite (H0 r). - unfold eval_branch_deps. rewrite VALCMP. + unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. -Qed. *) -(* -Theorem forward_simu_par_nextblockge ge fn rsr rsw mr mw sr sw sz rs' ex rs'' m'': - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - par_nextblock (Ptrofs.repr sz) rsr rsw = rs' -> - parexec_control ge fn ex rsr rs' mw = Next rs'' m'' -> - exists s'', - macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'' - /\ match_states (State rs'' m'') s''. *) + * intros rr; destruct rr; unfold par_nextblock; Simpl. + - simpl in *. inv MSR. inv MSW. inv H0. eexists. split. + rewrite (H1 PC). simpl. reflexivity. + split. Simpl. + intros rr. destruct rr; unfold par_nextblock; Simpl. +Qed. Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). +Lemma prun_iw_app_some: + forall c c' sr sw s' s'', + prun_iw Ge c sw sr = Some s' -> + prun_iw Ge c' s' sr = Some s'' -> + prun_iw Ge (c ++ c') sw sr = Some s''. +Proof. + induction c. + - simpl. intros. congruence. + - intros. simpl in *. destruct (macro_prun _ _ _ _); auto. eapply IHc; eauto. discriminate. +Qed. + Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> + parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' -> exists s', - prun_iw Ge (trans_block_aux bdy sz ex) sr sw = Some s' + prun_iw Ge (trans_block_aux bdy sz ex) sw sr = Some s' /\ match_states (State rs' m') s'. Proof. intros. unfold parexec_wio_bblock_aux in H2. unfold trans_block_aux. destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOB; try discriminate. exploit forward_simu_par_body. 4: eapply WIOB. all: eauto. intros (s' & RUNB & MS'). - destruct ex. - - exploit forward_simu_par_control. 4: eapply H2. all: eauto. -Admitted. - + exploit forward_simu_par_control. 4: eapply H2. all: eauto. + intros (s'' & RUNCTL & MS''). + eexists. split. + eapply prun_iw_app_some. eassumption. unfold prun_iw. rewrite RUNCTL. reflexivity. eassumption. +Qed. Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs' m' rs2 m2: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> + parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' -> parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 -> exists s2', - res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr) + res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr) /\ match_states (State rs2 m2) s2'. Admitted. @@ -1800,7 +1810,7 @@ Lemma forward_simu_par_wio_stuck_bdy1: Ge = Genv ge fn -> match_states (State rs m) s1' -> Permutation (bdy1 ++ bdy2) (body b) -> - parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> + parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs rs m m = Stuck -> res_eq None (prun_iw Ge (trans_block b) s1' s1'). Proof. Admitted. @@ -1809,7 +1819,7 @@ Lemma forward_simu_par_wio_stuck_bdy2 ge fn rs m s1' bdy1 bdy2 b m' rs': Ge = Genv ge fn -> match_states (State rs m) s1' -> Permutation (bdy1 ++ bdy2) (body b) -> - parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rs' m' -> + parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs rs m m = Next rs' m' -> parexec_wio_body ge bdy2 rs rs' m m' = Stuck -> res_eq None (prun_iw Ge (trans_block b) s1' s1'). Proof. @@ -1828,7 +1838,7 @@ Proof. inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). exploit trans_block_perserves_permutation; eauto. intros Perm. - remember (parexec_wio_bblock_aux _ _ _ _ _ _ _) as pwb. + remember (parexec_wio_bblock_aux _ _ _ _ _ _ _ _ _) as pwb. destruct pwb; try congruence. exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS'). unfold prun; eexists; split; eauto. @@ -1843,7 +1853,7 @@ Theorem forward_simu_par_stuck: Proof. intros until fn. intros GENV PAREXEC MS. inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). - destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT. + destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _ _ _) eqn:WIOEXIT. - econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy2; eauto. auto. - clear WIO. econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy1; eauto. auto. Qed. -- cgit From c4620aef8a80a9ca088493db5558b84bd3561052 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 27 Mar 2019 17:36:21 +0100 Subject: Proof of the entire forward simulation (still stuck to do + permutations) --- mppa_k1c/Asmblockdeps.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a65be8a8..2bd78449 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1773,9 +1773,16 @@ Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' -> parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 -> exists s2', - res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr) + prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr = Some s2' /\ match_states (State rs2 m2) s2'. -Admitted. +Proof. + intros. exploit forward_simu_par_wio_bblock_aux. 4: eapply H2. all: eauto. + intros (s' & RUNAUX & MS'). + exploit forward_simu_par_body. 4: eapply H3. all: eauto. + intros (s'' & RUNBDY2 & MS''). + eexists. split. + eapply prun_iw_app_some. eassumption. eassumption. eassumption. +Qed. Lemma trans_body_perserves_permutation bdy1 bdy2: Permutation bdy1 bdy2 -> @@ -1841,7 +1848,7 @@ Proof. remember (parexec_wio_bblock_aux _ _ _ _ _ _ _ _ _) as pwb. destruct pwb; try congruence. exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS'). - unfold prun; eexists; split; eauto. + unfold prun. unfold res_eq. eexists; split; eauto. Qed. Theorem forward_simu_par_stuck: -- cgit From 0b1ffa332effdc452b1c76dcbcc738908360f5a8 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 27 Mar 2019 17:45:08 +0100 Subject: dealing with permutations --- mppa_k1c/Asmblockdeps.v | 111 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 82 insertions(+), 29 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index df1acc6f..b608255f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1756,16 +1756,22 @@ Proof. Admitted. -Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs' m' rs2 m2: +Theorem forward_simu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz rs' m' rs2 m2: Ge = Genv ge fn -> match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr mr = Next rs' m' -> parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 -> exists s2', - res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr) + prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr = Some s2' /\ match_states (State rs2 m2) s2'. -Admitted. +Proof. + intros; exploit forward_simu_par_wio_bblock_aux. 4: eauto. all: eauto. + intros (s1' & X1 & X2). + exploit (forward_simu_par_body bdy2). 4: eauto. all: eauto. + intros (s2' & X3 & X4). + eexists; split; eauto. + erewrite prun_iw_app_Some; eauto. +Qed. Lemma trans_body_perserves_permutation bdy1 bdy2: Permutation bdy1 bdy2 -> @@ -1774,46 +1780,89 @@ Proof. induction 1; simpl; econstructor; eauto. Qed. +Lemma trans_body_app bdy1: forall bdy2, + trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2). +Proof. + induction bdy1; simpl; congruence. +Qed. + Theorem trans_block_perserves_permutation bdy1 bdy2 b: Permutation (bdy1 ++ bdy2) (body b) -> Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). +Proof. + intro H; unfold trans_block, trans_block_aux. + eapply perm_trans. + - eapply Permutation_app_tail. + apply trans_body_perserves_permutation. + apply Permutation_sym; eapply H. + - rewrite trans_body_app. rewrite <-! app_assoc. + apply Permutation_app_head. + apply Permutation_app_comm. +Qed. + +Lemma forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_basic_instr ge bi rsr rsw mr mw = Stuck -> + macro_prun Ge (trans_basic bi) sw sr sr = None. Admitted. -(* replaced by forward_simu_par_wio_bblock -Theorem forward_simu_par_wio: - forall ge fn rs1 m1 s1' bdy1 bdy2 b rs m rs2 m2 rs3 m3, +Lemma forward_simu_par_body_Stuck bdy: forall ge fn rsr mr sr rsw mw sw, Ge = Genv ge fn -> - match_states (State rs m) s1' -> - Permutation (bdy1 ++ bdy2) (body b) -> - parexec_wio_body ge bdy1 rs rs m m = Next rs1 m1 -> - parexec_control ge fn (exit b) rs (par_nextblock (Ptrofs.repr (size b)) rs rs1) m1 = Next rs2 m2 -> - parexec_wio_body ge bdy2 rs rs2 m m2 = Next rs3 m3 -> - exists s2', - res_eq (Some s2') (prun_iw Ge (trans_block b) s1' s1') - /\ match_states (State rs3 m3) s2'. + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_wio_body ge bdy rsr rsw mr mw = Stuck -> + prun_iw Ge (trans_body bdy) sw sr = None. Proof. + induction bdy. + - intros until sw. intros GENV MSR MSW WIO. + simpl in WIO. inv WIO. + - intros until sw. intros GENV MSR MSW WIO. + simpl in WIO. destruct (parexec_basic_instr _ _ _ _ _ _) eqn:PARBASIC. + * exploit forward_simu_par_wio_basic. 4: eapply PARBASIC. all: eauto. + intros (sw' & MPRUN & MS'). simpl prun_iw. rewrite MPRUN. + eapply IHbdy; eauto. + * exploit forward_simu_par_wio_basic_Stuck. 4: eapply PARBASIC. all: eauto. + intros X; simpl; rewrite X; auto. +Qed. + +Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck -> + macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. Admitted. -*) -Lemma forward_simu_par_wio_stuck_bdy1: - forall ge fn rs m s1' bdy1 bdy2 b, +Lemma forward_simu_par_wio_stuck_bdy1 ge fn rs m s1' bdy1 sz ex: Ge = Genv ge fn -> match_states (State rs m) s1' -> - Permutation (bdy1 ++ bdy2) (body b) -> - parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> - res_eq None (prun_iw Ge (trans_block b) s1' s1'). + parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs m = Stuck -> + prun_iw Ge ((trans_block_aux bdy1 sz ex)) s1' s1' = None. Proof. -Admitted. + unfold parexec_wio_bblock_aux, trans_block_aux; intros. + destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOB. + * exploit forward_simu_par_body. 4: eapply WIOB. all: eauto. + intros (s' & RUNB & MS'). + erewrite prun_iw_app_Some; eauto. + exploit forward_simu_par_control_Stuck. 4: eauto. all: eauto. + simpl. intros X; rewrite X. auto. + * apply prun_iw_app_None. eapply forward_simu_par_body_Stuck. 4: eauto. all: eauto. +Qed. -Lemma forward_simu_par_wio_stuck_bdy2 ge fn rs m s1' bdy1 bdy2 b m' rs': +Lemma forward_simu_par_wio_stuck_bdy2 ge fn rs m s1' bdy1 bdy2 sz ex m' rs': Ge = Genv ge fn -> match_states (State rs m) s1' -> - Permutation (bdy1 ++ bdy2) (body b) -> - parexec_wio_bblock_aux ge fn bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rs' m' -> + parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs m = Next rs' m' -> parexec_wio_body ge bdy2 rs rs' m m' = Stuck -> - res_eq None (prun_iw Ge (trans_block b) s1' s1'). + prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) s1' s1'=None. Proof. -Admitted. + intros; exploit forward_simu_par_wio_bblock_aux. 4: eauto. all: eauto. + intros (s2' & X1 & X2). + erewrite prun_iw_app_Some; eauto. + eapply forward_simu_par_body_Stuck. 4: eauto. all: eauto. +Qed. Theorem forward_simu_par: forall rs1 m1 s1' b ge fn rs2 m2, @@ -1831,7 +1880,7 @@ Proof. remember (parexec_wio_bblock_aux _ _ _ _ _ _ _) as pwb. destruct pwb; try congruence. exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS'). - unfold prun; eexists; split; eauto. + unfold prun; simpl; eexists; split; eauto. Qed. Theorem forward_simu_par_stuck: @@ -1843,9 +1892,13 @@ Theorem forward_simu_par_stuck: Proof. intros until fn. intros GENV PAREXEC MS. inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). + exploit trans_block_perserves_permutation; eauto. + intros Perm. destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT. - econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy2; eauto. auto. - - clear WIO. econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy1; eauto. auto. + - clear WIO. econstructor; eauto. split; eauto. + simpl; apply prun_iw_app_None; auto. + eapply forward_simu_par_wio_stuck_bdy1; eauto. Qed. Theorem forward_simu_par_alt: -- cgit