From 4807d6f32f08dd70f798a0478d39163ad3b81129 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 11 Apr 2019 14:20:56 +0200 Subject: refactor for #92 --- mppa_k1c/Asmblockdeps.v | 1094 ++++++++------------------ mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 28 +- mppa_k1c/abstractbb/Parallelizability.v | 8 +- 3 files changed, 338 insertions(+), 792 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 402e3178..a676d7b2 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -12,6 +12,7 @@ Require Import Coqlib. Require Import ImpDep. Require Import Axioms. Require Import Parallelizability. +Require Import Asmvliw Permutation. Open Scope impure. @@ -470,9 +471,6 @@ Import P. (** Compilation from Asmblock to L *) -Section SECT. -Variable Ge: genv. - Local Open Scope positive_scope. Definition pmem : R.t := 1. @@ -676,6 +674,17 @@ Proof. intros. congruence. Qed. +(** Parallelizability of a bblock (bundle) *) + +Module PChk := ParallelChecks L PosPseudoRegSet. + +Definition bblock_para_check (p: Asmvliw.bblock) : bool := + PChk.is_parallelizable (trans_block p). + +Section SECT_PAR. + +Import PChk. + Ltac Simplif := ((rewrite nextblock_inv by eauto with asmgen) || (rewrite nextblock_inv1 by eauto with asmgen) @@ -692,535 +701,394 @@ Ltac Simpl := repeat Simplif. Arguments Pos.add: simpl never. Arguments ppos: simpl never. -Theorem trans_state_match: forall S, match_states S (trans_state S). -Proof. - intros. destruct S as (rs & m). simpl. - split. reflexivity. - intro. destruct r; try reflexivity. - destruct g; reflexivity. -Qed. - -Lemma exec_app_some: - forall c c' s s' s'', - exec Ge c s = Some s' -> - exec Ge c' s' = Some s'' -> - exec Ge (c ++ c') s = Some s''. -Proof. - induction c. - - simpl. intros. congruence. - - intros. simpl in *. destruct (inst_run _ _ _ _); auto. eapply IHc; eauto. discriminate. -Qed. - -Lemma exec_app_none: - forall c c' s, - exec Ge c s = None -> - exec Ge (c ++ c') s = None. -Proof. - induction c. - - simpl. discriminate. - - intros. simpl. simpl in H. destruct (inst_run _ _ _ _); auto. -Qed. +Variable Ge: genv. -Lemma trans_arith_correct: - forall ge fn i rs m rs' s, - exec_arith_instr ge i rs = rs' -> - match_states (State rs m) s -> - exists s', - inst_run (Genv ge fn) (trans_arith i) s s = Some s' - /\ match_states (State rs' m) s'. +Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' 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' -> + exists sw', + inst_prun Ge (trans_arith i) sw sr sr = Some sw' + /\ match_states (State rsw' mw) sw'. Proof. - intros. unfold exec_arith_instr in H. unfold parexec_arith_instr in H. destruct i. + intros GENV MSR MSW PARARITH. subst. inv MSR. inv MSW. + unfold parexec_arith_instr. destruct i. (* Ploadsymbol *) - - inv H; inv H0. eexists; split; try split. + - destruct i. eexists; split; [| split]. + * simpl. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. + * simpl. intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRR *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rs0). rewrite e; reflexivity. + - eexists; split; [| split]. + * simpl. rewrite (H0 rs). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRI32 *) - - inv H. inv H0. - eexists; split; try split. + - eexists; split; [|split]. + * simpl. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRI64 *) - - inv H. inv H0. - eexists; split; try split. + - eexists; split; [|split]. + * simpl. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRF32 *) - - inv H. inv H0. - eexists; split; try split. + - eexists; split; [|split]. + * simpl. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRF64 *) - - inv H. inv H0. - eexists; split; try split. + - eexists; split; [|split]. + * simpl. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRRR *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rs1); rewrite e. pose (H1 rs2); rewrite e0. reflexivity. + - 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 *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rs0); rewrite e. reflexivity. + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithRRI64 *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rs0); rewrite e. reflexivity. + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithARRR *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rd); rewrite e. pose (H1 rs1); rewrite e0. pose (H1 rs2); rewrite e1. reflexivity. + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithARRI32 *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* PArithARRI64 *) - - inv H; inv H0; - eexists; split; try split. - * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. Qed. -Theorem forward_simu_basic_gen ge fn b rs m s: - match_states (State rs m) s -> - match_outcome (exec_basic_instr ge b rs m) (inst_run (Genv ge fn) (trans_basic b) s s). +Theorem forward_simu_par_wio_basic 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 -> + match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). Proof. - intros. destruct b; inversion H; simpl. + intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2). + destruct bi; simpl. (* Arith *) - - eapply trans_arith_correct; eauto. destruct i; simpl; reflexivity. + - exploit trans_arith_par_correct. 5: eauto. all: eauto. (* Load *) - destruct i. - (* Load Offset *) - + destruct i; simpl; - unfold parexec_load_offset; rewrite (H1 ra); rewrite H0; - destruct (eval_offset _ _); simpl; auto; destruct (Mem.loadv _ _); simpl; auto; - eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. - + destruct i; simpl; - unfold parexec_load_reg; rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_load_deps_reg; - destruct (Mem.loadv _ _); simpl; auto; - eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Load Offset *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; + destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Reg *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. (* Store *) - destruct i. - (* Store Offset *) - + destruct i; simpl; - rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold parexec_store_offset; destruct (eval_offset _ _); simpl; auto; - destruct (Mem.storev _ _ _ _); simpl; auto; - eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + (* Store Offset *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); + destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. - + destruct i; simpl; - rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold parexec_store_reg; unfold exec_store_deps_reg; - destruct (Mem.storev _ _ _ _); simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + (* Store Reg *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs); + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. (* Allocframe *) - - Simpl. rewrite (H1 SP). rewrite H0. destruct (Mem.alloc _ _ _) eqn:ALLOC; simpl; auto. destruct (Mem.store _ _ _ _) eqn:STORE; simpl; auto. - eexists; split; try split. - * Simpl. rewrite H0. rewrite ALLOC. rewrite STORE. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. - -(* Freeframe *) - - rewrite (H1 SP). rewrite H0. destruct (Mem.loadv _ _ _) eqn:LOAD; simpl; auto. destruct (rs GPR12) eqn:SPeq; simpl; auto. - destruct (Mem.free _ _ _ _) eqn:FREE; simpl; auto. Simpl. rewrite (H1 SP). eexists; split; try split. - * rewrite SPeq. rewrite LOAD. rewrite FREE. reflexivity. + - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. + * eexists; repeat split. + { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. + rewrite H, MEMAL. rewrite MEMS. reflexivity. } + { Simpl. } + { intros rr; destruct rr; Simpl. + destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. } + * simpl; Simpl; erewrite !H0, H, MEMAL, MEMS; auto. + (* Freeframe *) + - erewrite !H0, H. + destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto. + destruct (rsr GPR12) eqn:SPeq; simpl; auto. + destruct (Mem.free _ _ _ _) eqn:MFREE; simpl; auto. + eexists; repeat split. + * simpl. Simpl. erewrite H0, SPeq, MLOAD, MFREE. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. - + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. (* Pget *) - - destruct rs0; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. - + - destruct rs eqn:rseq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. (* Pset *) - - destruct rd; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - + - destruct rd eqn:rdeq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. (* Pnop *) - - eexists; split; try split. assumption. assumption. -Qed. - -Lemma forward_simu_basic ge fn b rs m rs' m' s: - exec_basic_instr ge b rs m = Next rs' m' -> - match_states (State rs m) s -> - exists s', - inst_run (Genv ge fn) (trans_basic b) s s = Some s' - /\ match_states (State rs' m') s'. -Proof. - intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H in H1. inv H1. eexists. eassumption. + - eexists. repeat split; assumption. Qed. -Lemma forward_simu_basic_instr_stuck i ge fn rs m s: - Ge = Genv ge fn -> - exec_basic_instr ge i rs m = Stuck -> - match_states (State rs m) s -> - exec Ge [trans_basic i] s = None. -Proof. - intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H0 in H2. inv H2. unfold exec. unfold run. rewrite H4. reflexivity. -Qed. -Lemma forward_simu_body: - forall bdy ge rs m rs' m' fn s, +Theorem forward_simu_par_body: + forall bdy ge fn rsr mr sr rsw mw sw, Ge = Genv ge fn -> - exec_body ge bdy rs m = Next rs' m' -> - match_states (State rs m) s -> - exists s', - exec Ge (trans_body bdy) s = Some s' - /\ match_states (State rs' m') s'. + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_wio_body ge bdy rsr rsw mr mw) (prun_iw Ge (trans_body bdy) sw sr). Proof. - induction bdy. - - intros. inv H1. simpl in *. inv H0. eexists. repeat (split; auto). - - intros until s. intros GE EXEB MS. simpl in EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate. - exploit forward_simu_basic; eauto. intros (s' & MRUN & MS'). subst Ge. - eapply IHbdy in MS'; eauto. destruct MS' as (s'' & EXECB & MS'). - eexists. split. - * simpl. rewrite MRUN. eassumption. - * eassumption. + induction bdy as [|i bdy]; simpl; eauto. + intros. + exploit (forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto. + destruct (parexec_basic_instr _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). rewrite X1; simpl; eauto. + - intros X; rewrite X; simpl; auto. Qed. -Theorem forward_simu_control_gen ge fn ex b rs m s: +Theorem forward_simu_par_control ex sz aux ge fn rsr rsw mr mw sr sw: Ge = Genv ge fn -> - match_states (State rs m) s -> - match_outcome (exec_control ge fn ex (nextblock b rs) m) (exec Ge (trans_pcincr (size b) (trans_exit ex) :: nil) s). + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) (rsw#PC <- aux) mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros. destruct ex; simpl; inv H0. - - destruct c; destruct i; simpl; rewrite (H2 PC); auto. - all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock, incrPC; Simpl). + intros GENV MSR MSW; unfold parexec_exit. + simpl in *. inv MSR. inv MSW. + destruct ex. + - destruct c; destruct i; try discriminate; simpl. + all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl). (* Pjumptable *) - + Simpl. rewrite (H2 r). destruct (rs r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. - unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl. + destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. + unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - destruct (preg_eq GPR62 g). rewrite e. Simpl. - destruct (preg_eq GPR63 g). rewrite e. Simpl. Simpl. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. + destruct (preg_eq g GPR62). rewrite e. Simpl. + destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. (* Pj_l *) - + Simpl. unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. - unfold nextblock, incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. + + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. + unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. (* Pcb *) - + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps. - ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b0. - +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b0. - +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. + + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. + ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. (* Pcbu *) - + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps. - ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b0. - +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b0. - +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. - - - simpl. rewrite (H2 PC). eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. -Qed. + + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. + ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. -Lemma forward_simu_control ge fn ex b rs m rs2 m2 s: - Ge = Genv ge fn -> - 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) :: nil) s = Some s' - /\ match_states (State rs2 m2) s'. -Proof. - intros. exploit (forward_simu_control_gen); eauto. intros. - rewrite H0 in H2. inv H2. eexists. eapply H3. + - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl. + intros rr; destruct rr; unfold incrPC; Simpl. Qed. -Lemma forward_simu_control_stuck: - forall ge fn rs m s ex b, +Theorem forward_simu_par_exit ex sz ge fn rsr rsw mr mw sr sw: Ge = Genv ge fn -> - match_states (State rs m) s -> - exec Ge (trans_pcincr (size b) (trans_exit ex) :: nil) s = None -> - exec_control ge fn ex (nextblock b rs) m = Stuck. -Proof. - intros. exploit (forward_simu_control_gen); eauto. intros. - rewrite H1 in H2. destruct (exec_control _ _ _ _ _); auto. inv H2. inv H3. discriminate. -Qed. - -Theorem forward_simu: - forall rs1 m1 rs2 m2 s1' b ge fn, - Ge = Genv ge fn -> - exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> - match_states (State rs1 m1) s1' -> - exists s2', - exec Ge (trans_block b) s1' = Some s2' - /\ match_states (State rs2 m2) s2'. + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_exit ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros until fn. intros GENV EXECB MS. unfold exec_bblock in EXECB. destruct (exec_body _ _ _) eqn:EXEB; try discriminate. - exploit forward_simu_body; eauto. intros (s' & EXETRANSB & MS'). - exploit forward_simu_control; eauto. intros (s'' & EXETRANSEX & MS''). - - eexists. split. - unfold trans_block. eapply exec_app_some. eassumption. eassumption. - eassumption. + intros; unfold parexec_exit. + exploit (forward_simu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto. + cutrewrite (rsw # PC <- (rsw PC) = rsw); auto. + apply extensionality. intros; destruct x; simpl; auto. Qed. -Lemma exec_bblock_stuck_nec: - forall ge fn b rs m, - exec_body ge (body b) rs m = Stuck - \/ (exists rs' m', exec_body ge (body b) rs m = Next rs' m' /\ exec_control ge fn (exit b) (nextblock b rs') m' = Stuck) - <-> exec_bblock ge fn b rs m = Stuck. -Proof. - intros. split. - + intros. destruct H. - - unfold exec_bblock. rewrite H. reflexivity. - - destruct H as (rs' & m' & EXEB & EXEC). unfold exec_bblock. rewrite EXEB. assumption. - + intros. unfold exec_bblock in H. destruct (exec_body _ _ _ _) eqn:EXEB. - - right. repeat eexists. assumption. - - left. reflexivity. -Qed. +Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). -Lemma exec_basic_instr_next_exec: - forall ge fn i rs m rs' m' s tc, +Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz: Ge = Genv ge fn -> - exec_basic_instr ge i rs m = Next rs' m' -> - match_states (State rs m) s -> - exists s', - exec Ge (trans_basic i :: tc) s = exec Ge tc s' - /\ match_states (State rs' m') s'. + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr rsw mr mw) (prun_iw Ge (trans_block_aux bdy sz ex) sw sr). Proof. - intros. exploit forward_simu_basic; eauto. - intros (s' & MRUN & MS'). - simpl exec. exists s'. subst. rewrite MRUN. split; auto. + intros GENV MSR MSW. unfold parexec_wio_bblock_aux, trans_block_aux. + exploit (forward_simu_par_body bdy ge fn rsr mr sr rsw mw sw); eauto. + destruct (parexec_wio_body _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite prun_iw_app_Some; eauto. + exploit (forward_simu_par_exit ex sz ge fn rsr rs mr m sr s'); eauto. + subst Ge; simpl. destruct MSR as (Y1 & Y2). erewrite Y2; simpl. + destruct (inst_prun _ _ _ _ _); simpl; auto. + - intros X; erewrite prun_iw_app_None; eauto. Qed. -Lemma exec_body_next_exec: - forall c ge fn rs m rs' m' s tc, +Theorem forward_simu_par_wio_bblock ge fn rsr rsw mr sr sw mw bdy1 bdy2 ex sz: Ge = Genv ge fn -> - exec_body ge c rs m = Next rs' m' -> - match_states (State rs m) s -> - exists s', - exec Ge (trans_body c ++ tc) s = exec Ge tc s' - /\ match_states (State rs' m') s'. + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome + match parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw with + | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m' + | Stuck => Stuck + end + (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr). Proof. - induction c. - - intros. simpl in H0. inv H0. simpl. exists s. split; auto. - - intros. simpl in H0. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate. - exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEBASIC & MS'). - simpl trans_body. rewrite <- app_comm_cons. rewrite EXEGEBASIC. - eapply IHc; eauto. + intros. + exploit (forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy1 ex sz); eauto. + destruct (parexec_wio_bblock_aux _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite prun_iw_app_Some; eauto. + eapply forward_simu_par_body; eauto. + - intros; erewrite prun_iw_app_None; eauto. Qed. -Lemma exec_trans_pcincr_exec_instrun: - forall rs m s b k, - match_states (State rs m) s -> - exists s', - inst_run Ge ((# PC, Op (OIncremPC (size b)) (PReg(# PC) @ Enil)) :: k) s s = inst_run Ge k s' s - /\ match_states (State (nextblock b rs) m) s'. +Lemma trans_body_perserves_permutation bdy1 bdy2: + Permutation bdy1 bdy2 -> + Permutation (trans_body bdy1) (trans_body bdy2). Proof. - intros. inv H. eexists. split. simpl. pose (H1 PC); simpl in e; rewrite e. destruct Ge. simpl. eapply eq_refl. - simpl. split. - - Simpl. - - intros rr; destruct rr; Simpl. + induction 1; simpl; econstructor; eauto. Qed. -Lemma inst_run_trans_exit_noold: - forall ex s s' s'', - inst_run Ge (trans_exit ex) s s' = inst_run Ge (trans_exit ex) s s''. +Lemma trans_body_app bdy1: forall bdy2, + trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2). Proof. - intros. destruct ex. - - destruct c; destruct i; reflexivity. - - reflexivity. + induction bdy1; simpl; congruence. Qed. -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)) :: nil) s = exec Ge [trans_exit (exit b)] s' - /\ match_states (State (nextblock b rs) m) s'. +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. - intros. - exploit exec_trans_pcincr_exec_instrun; eauto. - intros (s' & MRUN & MS). - eexists. split. unfold exec. unfold trans_pcincr. unfold run. rewrite MRUN. - erewrite inst_run_trans_exit_noold; eauto. - assumption. + 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 exec_exit_none: - forall ge fn rs m s ex, - Ge = Genv ge fn -> - match_states (State rs m) s -> - exec Ge [trans_exit ex] s = None -> - exec_control ge fn ex rs m = Stuck. -Proof. - intros. inv H0. destruct ex as [ctl|]; try discriminate. - destruct ctl; destruct i; try reflexivity; try discriminate. -(* Pjumptable *) - - simpl in *. repeat (rewrite H3 in H1). - destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto. - unfold goto_label_deps in H1. unfold par_goto_label. Simpl. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. -(* Pj_l *) - - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e. - unfold goto_label_deps in H1. unfold par_goto_label. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. -(* Pcb *) - - simpl in *. destruct (cmp_for_btest bt). destruct i. - + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. - unfold eval_branch_deps in H1; unfold par_eval_branch. - destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate. - unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto. - destruct (rs PC); auto. discriminate. - + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. - unfold eval_branch_deps in H1; unfold par_eval_branch. - destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate. - unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto. - destruct (rs PC); auto. discriminate. -(* Pcbu *) - - simpl in *. destruct (cmpu_for_btest bt). destruct i. - + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. - pose (H3 r); simpl in e; rewrite e in H1; clear e. - unfold eval_branch_deps in H1; unfold par_eval_branch. - destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate. - unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto. - destruct (rs PC); auto. discriminate. - + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. - pose (H3 r); simpl in e; rewrite e in H1; clear e. - unfold eval_branch_deps in H1; unfold par_eval_branch. - destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate. - unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto. - destruct (rs PC); auto. discriminate. +Theorem forward_simu_par 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 GENV MS PAREXEC. + inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). + exploit trans_block_perserves_permutation; eauto. + intros Perm. + exploit (forward_simu_par_wio_bblock ge fn rs1 rs1 m1 s1' s1' m1 bdy1 bdy2 (exit b) (size b)); eauto. + rewrite <- WIO. clear WIO. + intros H; eexists; split. 2: eapply H. + unfold prun; eexists; split; eauto. + destruct (prun_iw _ _ _ _); simpl; eauto. Qed. -Theorem trans_block_reverse_stuck: - forall ge fn b rs m s, +(* sequential execution *) +Theorem forward_simu_basic ge fn bi rs m s: Ge = Genv ge fn -> - exec Ge (trans_block b) s = None -> match_states (State rs m) s -> - exec_bblock ge fn b rs m = Stuck. + match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s). Proof. - intros until s. intros Geq EXECBK MS. - apply exec_bblock_stuck_nec. - destruct (exec_body _ _ _ _) eqn:EXEB. - - right. repeat eexists. - exploit exec_body_next_exec; eauto. - intros (s' & EXECBK' & MS'). unfold trans_block in EXECBK. rewrite EXECBK' in EXECBK. clear EXECBK'. clear EXEB MS. - eapply forward_simu_control_stuck; eauto. - - left. reflexivity. + intros; unfold exec_basic_instr. rewrite inst_run_prun. + eapply forward_simu_par_wio_basic; eauto. Qed. -Lemma forward_simu_body_stuck: +Lemma forward_simu_body: forall bdy ge fn rs m s, Ge = Genv ge fn -> - exec_body ge bdy rs m = Stuck -> match_states (State rs m) s -> - exec Ge (trans_body bdy) s = None. + match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s). Proof. - induction bdy. - - simpl. discriminate. - - intros. simpl trans_body. simpl in H0. - destruct (exec_basic_instr _ _ _ _) eqn:EBI. - + exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEB & MS'). rewrite EXEGEB. eapply IHbdy; eauto. - + cutrewrite (trans_basic a :: trans_body bdy = (trans_basic a :: nil) ++ trans_body bdy); try reflexivity. apply exec_app_none. - eapply forward_simu_basic_instr_stuck; eauto. + induction bdy as [|i bdy]; simpl; eauto. + intros. + exploit (forward_simu_basic ge fn i rs m s); eauto. + destruct (exec_basic_instr _ _ _ _); simpl. + - intros (s' & X1 & X2). rewrite X1; simpl; eauto. + - intros X; rewrite X; simpl; auto. Qed. - -Lemma forward_simu_exit_stuck: - forall ex ge fn rs m s, +Theorem forward_simu_exit ge fn b rs m s: Ge = Genv ge fn -> - exec_control ge fn ex rs m = Stuck -> match_states (State rs m) s -> - exec Ge [(trans_exit ex)] s = None. + match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s). Proof. - intros. inv H1. destruct ex as [ctl|]; try discriminate. - destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). - (* Pjumptable *) - - simpl in *. repeat (rewrite H3). destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto. - unfold goto_label_deps. unfold par_goto_label in H0. - destruct (label_pos _ _ _); auto. repeat (rewrite Pregmap.gso in H0; try discriminate). destruct (rs PC); auto. discriminate. -(* Pj_l *) - - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold par_goto_label in H0. - destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate. -(* Pcb *) - - simpl in *. destruct (cmp_for_btest bt). destruct i. - -- destruct o. - + unfold par_eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmp_bool _ _ _); auto. - destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. - -- destruct o. - + unfold par_eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpl_bool _ _ _); auto. - destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. -(* Pcbu *) - - simpl in *. destruct (cmpu_for_btest bt). destruct i. - -- destruct o. - + unfold par_eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmpu_bool _ _); auto. - destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. - -- destruct o. - + unfold par_eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmplu_bool _ _); auto. - destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0. - destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. + intros; unfold exec_control, nextblock. rewrite inst_run_prun. + apply (forward_simu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto. Qed. - -Theorem forward_simu_stuck: - forall rs1 m1 s1' b ge fn, +Theorem forward_simu rs m b ge fn s: Ge = Genv ge fn -> - exec_bblock ge fn b rs1 m1 = Stuck -> - match_states (State rs1 m1) s1' -> - exec Ge (trans_block b) s1' = None. + match_states (State rs m) s -> + match_outcome (exec_bblock ge fn b rs m) (exec Ge (trans_block b) s). +Proof. + intros GENV MS. unfold exec_bblock. + exploit (forward_simu_body (body b) ge fn rs m s); eauto. + unfold exec, trans_block; simpl. + destruct (exec_body _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite run_app_Some; eauto. + exploit (forward_simu_exit ge fn b rs0 m0 s'); eauto. + subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl. + destruct (inst_run _ _ _); simpl; auto. + - intros X; erewrite run_app_None; eauto. +Qed. + + +Theorem trans_state_match: forall S, match_states S (trans_state S). Proof. - intros until fn. intros GENV EXECB MS. apply exec_bblock_stuck_nec in EXECB. destruct EXECB. - - unfold trans_block. apply exec_app_none. eapply forward_simu_body_stuck; eauto. - - destruct H as (rs' & m' & EXEB & EXEC). unfold trans_block. exploit exec_body_next_exec; eauto. - intros (s' & EXEGEBODY & MS'). rewrite EXEGEBODY. exploit exec_trans_pcincr_exec; eauto. - intros (s'' & EXEGEPC & MS''). rewrite EXEGEPC. eapply forward_simu_exit_stuck; eauto. + intros. destruct S as (rs & m). simpl. + split. reflexivity. + intro. destruct r; try reflexivity. + destruct g; reflexivity. Qed. @@ -1230,26 +1098,47 @@ Proof. intros. congruence. Qed. -Theorem state_equiv: - forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2. +Theorem state_equiv S1 S2 S': match_states S1 S' -> match_states S2 S' -> S1 = S2. Proof. - intros. inv H. unfold match_states in H0, H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1. + unfold match_states; intros H0 H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1. apply state_eq_decomp. - apply functional_extensionality. intros. assert (Val (rs1 x) = Val (rs2 x)) by congruence. congruence. - congruence. Qed. -Theorem forward_simu_alt: - forall rs1 m1 s1' b ge fn, - Ge = Genv ge fn -> - match_states (State rs1 m1) s1' -> - match_outcome (exec_bblock ge fn b rs1 m1) (exec Ge (trans_block b) s1'). +Lemma bblock_para_check_correct ge fn bb rs m rs' m': + Ge = Genv ge fn -> + exec_bblock ge fn bb rs m = Next rs' m' -> + bblock_para_check bb = true -> + det_parexec ge fn bb rs m rs' m'. Proof. - intros until fn. intros GENV MS. destruct (exec_bblock _ _ _ _ _) eqn:EXEB. - - eapply forward_simu; eauto. - - eapply forward_simu_stuck; eauto. + intros H H0 H1 o H2. unfold bblock_para_check in H1. + exploit (forward_simu rs m bb ge fn); eauto. eapply trans_state_match. + rewrite H0; simpl. + intros (s2' & EXEC & MS). + exploit forward_simu_par. 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; unfold trans_state in H. + 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 (State rs' m') (State rs0 m0)). + 2: eapply H4. eapply MS. intro H. inv H. reflexivity. + - unfold match_outcome in MO. destruct o. + + inv MO. inv H3. discriminate. + + clear MO. unfold exec in EXEC. + unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate. Qed. +End SECT_PAR. + + +Section SECT_BBLOCK_EQUIV. + +Variable Ge: genv. + Local Hint Resolve trans_state_match. Lemma bblock_equiv_reduce: @@ -1262,8 +1151,8 @@ Proof. intros rs m. generalize (H2 (trans_state (State rs m))); clear H2. intro H2. - exploit (forward_simu_alt rs m (trans_state (State rs m)) p1 ge fn); eauto. - exploit (forward_simu_alt rs m (trans_state (State rs m)) p2 ge fn); eauto. + exploit (forward_simu Ge rs m p1 ge fn (trans_state (State rs m))); eauto. + exploit (forward_simu Ge rs m p2 ge fn (trans_state (State rs m))); eauto. remember (exec_bblock ge fn p1 rs m) as exp1. destruct exp1. + (* Next *) @@ -1572,377 +1461,8 @@ Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bbloc Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. -End SECT. - -(** Parallelizability of a bblock *) - -Module PChk := ParallelChecks L PosPseudoRegSet. - -Definition bblock_para_check (p: Asmvliw.bblock) : bool := - PChk.is_parallelizable (trans_block p). - -Require Import Asmvliw Permutation. -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. +End SECT_BBLOCK_EQUIV. -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' 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' -> - exists sw', - inst_prun Ge (trans_arith i) sw sr sr = Some sw' - /\ match_states (State rsw' mw) sw'. -Proof. - intros GENV MSR MSW PARARITH. 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. -(* PArithARRR *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARRI32 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARRI64 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). 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: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). -Proof. - intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2). - destruct bi; simpl. -(* Arith *) - - exploit trans_arith_par_correct. 5: eauto. all: eauto. -(* Load *) - - destruct i. - (* Load Offset *) - + destruct i; simpl load_chunk. all: - unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; - destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; - eexists; split; try split; Simpl; - intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. - - (* Load Reg *) - + destruct i; simpl load_chunk. all: - unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs); - destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; - eexists; split; try split; Simpl; - intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. - -(* Store *) - - destruct i. - (* Store Offset *) - + destruct i; simpl store_chunk. all: - unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; - destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; - eexists; split; try split; Simpl; - intros rr; destruct rr; Simpl. - - (* Store Reg *) - + destruct i; simpl store_chunk. all: - unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs); - destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; - eexists; split; try split; Simpl; - intros rr; destruct rr; Simpl. - -(* Allocframe *) - - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. - * eexists; repeat split. - { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. - rewrite H, MEMAL. rewrite MEMS. reflexivity. } - { Simpl. } - { intros rr; destruct rr; Simpl. - destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. } - * simpl; Simpl; erewrite !H0, H, MEMAL, MEMS; auto. - (* Freeframe *) - - erewrite !H0, H. - destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto. - destruct (rsr GPR12) eqn:SPeq; simpl; auto. - destruct (Mem.free _ _ _ _) eqn:MFREE; simpl; auto. - eexists; repeat split. - * simpl. Simpl. erewrite H0, SPeq, MLOAD, MFREE. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. -(* Pget *) - - destruct rs eqn:rseq; simpl; auto. - eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* Pset *) - - destruct rd eqn:rdeq; simpl; auto. - eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. -(* Pnop *) - - eexists. repeat split; assumption. -Qed. - - -Theorem forward_simu_par_body: - forall bdy ge fn rsr mr sr rsw mw sw, - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - match_outcome (parexec_wio_body ge bdy rsr rsw mr mw) (prun_iw Ge (trans_body bdy) sw sr). -Proof. - induction bdy as [|i bdy]; simpl; eauto. - intros. - exploit (forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto. - destruct (parexec_basic_instr _ _ _ _ _ _); simpl. - - intros (s' & X1 & X2). rewrite X1; simpl; eauto. - - intros X; rewrite X; simpl; auto. -Qed. - -Theorem forward_simu_par_control ex sz ge fn rsr rsw mr mw sr sw: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). -Proof. - intros GENV MSR MSW. - simpl in *. inv MSR. inv MSW. - destruct ex. - - destruct c; destruct i; try discriminate; simpl. - all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl). - - (* Pjumptable *) - + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl. - destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. - unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. - destruct (preg_eq g GPR62). rewrite e. Simpl. - destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. - - (* Pj_l *) - + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. - unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. - - (* Pcb *) - + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto. - unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. - ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b. - +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. - intros rr; destruct rr; Simpl. - +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b. - +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. - intros rr; destruct rr; Simpl. - +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - - (* Pcbu *) - + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. - unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. - ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. - +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. - intros rr; destruct rr; Simpl. - +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. - +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. - destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. - intros rr; destruct rr; Simpl. - +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - - - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl. - intros rr; destruct rr; unfold incrPC; Simpl. -Qed. - -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: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - match_outcome (parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr rsw mr mw) (prun_iw Ge (trans_block_aux bdy sz ex) sw sr). -Proof. - intros H H0 H1. unfold parexec_wio_bblock_aux, trans_block_aux. - exploit (forward_simu_par_body bdy ge fn rsr mr sr rsw mw sw); eauto. - destruct (parexec_wio_body _ _ _ _ _ _); simpl. - - intros (s' & X1 & X2). - erewrite prun_iw_app_Some; eauto. - unfold parexec_exit. - exploit (forward_simu_par_control ex sz ge fn rsr rs mr m sr s'); eauto. - subst Ge; simpl. destruct H0 as (Y1 & Y2). erewrite Y2; simpl. - destruct (inst_prun _ _ _ _ _); simpl; auto. - - intros X; erewrite prun_iw_app_None; eauto. -Qed. - -Theorem forward_simu_par_wio_bblock ge fn rsr rsw mr sr sw mw bdy1 bdy2 ex sz: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - match_outcome - match parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw with - | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m' - | Stuck => Stuck - end - (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr). -Proof. - intros H H0 H1. - exploit (forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy1 ex sz); eauto. - destruct (parexec_wio_bblock_aux _ _ _ _ _ _); simpl. - - intros (s' & X1 & X2). - erewrite prun_iw_app_Some; eauto. - eapply forward_simu_par_body; eauto. - - intros X; erewrite prun_iw_app_None; eauto. -Qed. - -Lemma trans_body_perserves_permutation bdy1 bdy2: - Permutation bdy1 bdy2 -> - Permutation (trans_body bdy1) (trans_body bdy2). -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. - -Theorem forward_simu_par 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 GENV MS PAREXEC. - inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). - exploit trans_block_perserves_permutation; eauto. - intros Perm. - exploit (forward_simu_par_wio_bblock ge fn rs1 rs1 m1 s1' s1' m1 bdy1 bdy2 (exit b) (size b)); eauto. - rewrite <- WIO. clear WIO. - intros H; eexists; split. 2: eapply H. - unfold prun; eexists; split; eauto. - destruct (prun_iw _ _ _ _); simpl; eauto. -Qed. - - -Lemma bblock_para_check_correct ge fn bb rs m rs' m': - Ge = Genv ge fn -> - exec_bblock ge fn bb rs m = Next rs' m' -> - bblock_para_check bb = true -> - det_parexec ge fn bb rs m rs' m'. -Proof. - intros H H0 H1 o H2. unfold bblock_para_check in H1. - exploit forward_simu; eauto. eapply trans_state_match. - intros (s2' & EXEC & MS). - exploit forward_simu_par. 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_PAR. diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 3023ad8a..d1950209 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -211,7 +211,33 @@ Proof. intros; eapply res_eq_trans. eapply alt_bblock_equiv_refl; eauto. eauto. Qed. - + + +Lemma run_app p1: forall m1 p2, + run (p1++p2) m1 = + match run p1 m1 with + | Some m2 => run p2 m2 + | None => None + end. +Proof. + induction p1; simpl; try congruence. + intros; destruct (inst_run _ _ _); simpl; auto. +Qed. + +Lemma run_app_None p1 m1 p2: + run p1 m1 = None -> + run (p1++p2) m1 = None. +Proof. + intro H; rewrite run_app. rewrite H; auto. +Qed. + +Lemma run_app_Some p1 m1 m2 p2: + run p1 m1 = Some m2 -> + run (p1++p2) m1 = run p2 m2. +Proof. + intros H; rewrite run_app. rewrite H; auto. +Qed. + End SEQLANG. End MkSeqLanguage. diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index d1971e57..eae7b672 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -91,18 +91,18 @@ Proof. intros; destruct (inst_prun _ _ _); simpl; auto. Qed. -Lemma prun_iw_app_None p1: forall m1 old p2, +Lemma prun_iw_app_None p1 m1 old p2: prun_iw p1 m1 old = None -> prun_iw (p1++p2) m1 old = None. Proof. - intros m1 old p2 H; rewrite prun_iw_app. rewrite H; auto. + intros H; rewrite prun_iw_app. rewrite H; auto. Qed. -Lemma prun_iw_app_Some p1: forall m1 old m2 p2, +Lemma prun_iw_app_Some p1 m1 old m2 p2: prun_iw p1 m1 old = Some m2 -> prun_iw (p1++p2) m1 old = prun_iw p2 m2 old. Proof. - intros m1 old m2 p2 H; rewrite prun_iw_app. rewrite H; auto. + intros H; rewrite prun_iw_app. rewrite H; auto. Qed. End PARALLEL. -- cgit From 1d7796d6d39eb9d7ff79ac3d1fee1e107ce204f4 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 11 Apr 2019 14:38:20 +0200 Subject: more robust pattern-matching in *op_eq --- mppa_k1c/Asmblockdeps.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a676d7b2..4559dd62 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -346,10 +346,11 @@ Hint Resolve arith_op_eq_correct: wlp. Opaque arith_op_eq_correct. Definition load_op_eq (o1 o2: load_op): ?? bool := - match o1, o2 with - | OLoadRRO n1 ofs1, OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) - | OLoadRRR n1, OLoadRRR n2 => phys_eq n1 n2 - | _, _ => RET false + match o1 with + | OLoadRRO n1 ofs1 => + match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + | OLoadRRR n1 => + match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end end. Lemma load_op_eq_correct o1 o2: @@ -364,10 +365,11 @@ Opaque load_op_eq_correct. Definition store_op_eq (o1 o2: store_op): ?? bool := - match o1, o2 with - | OStoreRRO n1 ofs1, OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) - | OStoreRRR n1, OStoreRRR n2 => phys_eq n1 n2 - | _, _ => RET false + match o1 with + | OStoreRRO n1 ofs1 => + match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + | OStoreRRR n1 => + match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end end. Lemma store_op_eq_correct o1 o2: -- cgit From b42e3f8b36c5b3d8511f3428fce4190bbec73d19 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 11 Apr 2019 15:34:05 +0200 Subject: update from Impure Library --- mppa_k1c/abstractbb/Impure/ImpLoops.v | 42 ++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 20 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/abstractbb/Impure/ImpLoops.v b/mppa_k1c/abstractbb/Impure/ImpLoops.v index 9e11195e..dc8b2627 100644 --- a/mppa_k1c/abstractbb/Impure/ImpLoops.v +++ b/mppa_k1c/abstractbb/Impure/ImpLoops.v @@ -11,38 +11,38 @@ Local Open Scope impure. Axiom loop: forall {A B}, A * (A -> ?? (A+B)) -> ?? B. Extract Constant loop => "ImpLoopOracles.loop". -(** A while loop *) -Record while_loop_invariant {S} (cond: S -> bool) (body: S -> ?? S) (s0: S) (I: S -> Prop): Prop := - { while_init: I s0; - while_preserv s: I s -> cond s = true -> WHEN (body s) ~> s' THEN I s' - }. -Arguments while_init [S cond body s0 I]. -Arguments while_preserv [S cond body s0 I]. +Section While_Loop. -Program Definition while {S} cond body s0 (I: S -> Prop | while_loop_invariant cond body s0 I): ?? {s | I s /\ cond s = false} - := loop (A:={s | I s}) +(** Local Definition of "while-loop-invariant" *) +Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'. + +Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | I s0 -> I s /\ cond s = false} + := loop (A:={s | I s0 -> I s}) (s0, fun s => match (cond s) with | true => DO s' <~ mk_annot (body s) ;; - RET (inl (A:={s | I s }) s') + RET (inl (A:={s | I s0 -> I s }) s') | false => - RET (inr (B:={s | I s /\ cond s = false}) s) + RET (inr (B:={s | I s0 -> I s /\ cond s = false}) s) end). -Obligation 1. - destruct H; auto. -Qed. Obligation 2. - eapply (while_preserv H1); eauto. + unfold wli, wlp in * |-; eauto. Qed. Extraction Inline while. -(** A loop until None (useful to demonstrate a UNSAT property) *) +End While_Loop. -Program Definition loop_until_None {S} (I: S -> Prop) (body: S -> ?? (option S)) - (H:forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end) (s0:S): ?? ~(I s0) + +Section Loop_Until_None. +(** useful to demonstrate a UNSAT property *) + +(** Local Definition of "loop-until-None-invariant" *) +Let luni {S} (body: S -> ?? (option S)) (I: S -> Prop) := forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end. + +Program Definition loop_until_None {S} body (I: S -> Prop | luni body I) s0: ?? ~(I s0) := loop (A:={s | I s0 -> I s}) (s0, fun s => @@ -52,13 +52,15 @@ Program Definition loop_until_None {S} (I: S -> Prop) (body: S -> ?? (option S)) | None => RET (inr (B:=~(I s0)) _) end). Obligation 2. - refine (H s _ _ H1). auto. + refine (H2 s _ _ H0). auto. Qed. Obligation 3. - intros X; refine (H s _ _ H0). auto. + intros X; refine (H1 s _ _ H). auto. Qed. Extraction Inline loop_until_None. +End Loop_Until_None. + (*********************************************) (* A generic fixpoint from an equality test *) -- cgit