From afa25aac9373e4a7b37433ed861257a630264c29 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 14 Mar 2019 11:42:11 +0100 Subject: definition of VLIW semantics --- mppa_k1c/Asmblock.v | 18 +- mppa_k1c/Asmvliw.v | 329 +++++++++++++++++++++++++++++++++++++ mppa_k1c/PostpassSchedulingproof.v | 9 +- 3 files changed, 342 insertions(+), 14 deletions(-) create mode 100644 mppa_k1c/Asmvliw.v (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 621ed8a7..b656789b 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -801,10 +801,10 @@ Section RELSEM. set and memory state after execution of the instruction at [rs#PC], or [Stuck] if the processor is stuck. *) -Inductive outcome {rgset}: Type := - | Next (rs:rgset) (m:mem) +Inductive outcome: Type := + | Next (rs:regset) (m:mem) | Stuck. -Arguments outcome: clear implicits. +(* Arguments outcome: clear implicits. *) (** ** Arithmetic Expressions (including comparisons) *) @@ -1221,7 +1221,7 @@ Definition store_chunk n := (** * basic instructions *) -Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset := +Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := match bi with | PArith ai => Next (exec_arith_instr ai rs) m @@ -1263,7 +1263,7 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset : | Pnop => Next rs m end. -Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome regset := +Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with | nil => Next rs m | bi::body' => @@ -1323,7 +1323,7 @@ Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' end. -Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome regset := +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := match label_pos lbl 0 (fn_blocks f) with | None => Stuck | Some pos => @@ -1338,7 +1338,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome Warning: in m PC is assumed to be already pointing on the next instruction ! *) -Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome regset := +Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := match res with | Some true => goto_label f l rs m | Some false => Next rs m @@ -1362,7 +1362,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti we generate cannot use those registers to hold values that must survive the execution of the pseudo-instruction. *) -Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome regset := +Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := match oc with | Some ic => (** Get/Set system registers *) @@ -1403,7 +1403,7 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) | None => Next rs m end. -Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome regset := +Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome := match exec_body (body b) rs0 m with | Next rs' m' => let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m' diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v new file mode 100644 index 00000000..2c88673b --- /dev/null +++ b/mppa_k1c/Asmvliw.v @@ -0,0 +1,329 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Prashanth Mundkur, SRI International *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* The contributions by Prashanth Mundkur are reused and adapted *) +(* under the terms of a Contributor License Agreement between *) +(* SRI International and INRIA. *) +(* *) +(* *********************************************************************) + +(** Abstract syntax and semantics for K1c assembly language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Locations. +Require Stacklayout. +Require Import Conventions. +Require Import Errors. +Require Import Asmblock. + +Local Open Scope asm. + +Section RELSEM. + +(** Execution of arith instructions *) + +Variable ge: genv. + +(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code + en définissant + exec_arith_instr ai rs := parexec_arith_instr ai rs rs +*) +Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := + match ai with + | PArithR n d => rsw#d <- (arith_eval_r ge n) + + | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s) + + | PArithRI32 n d i => rsw#d <- (arith_eval_ri32 n i) + | PArithRI64 n d i => rsw#d <- (arith_eval_ri64 n i) + | PArithRF32 n d i => rsw#d <- (arith_eval_rf32 n i) + | PArithRF64 n d i => rsw#d <- (arith_eval_rf64 n i) + + | PArithRRR n d s1 s2 => rsw#d <- (arith_eval_rrr n rsr#s1 rsr#s2) + + | PArithRRI32 n d s i => rsw#d <- (arith_eval_rri32 n rsr#s i) + + | PArithRRI64 n d s i => rsw#d <- (arith_eval_rri64 n rsr#s i) + end. + +(** * load/store *) + +(* TODO: factoriser ? *) +Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) + (d: ireg) (a: ireg) (ofs: offset) := + match (eval_offset ge ofs) with + | OK ptr => + match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with + | None => Stuck + | Some v => Next (rsw#d <- v) mw + end + | _ => Stuck + end. + +(* rem: parexec_store = exec_store *) + +(** * basic instructions *) + +(* TODO: factoriser ? *) +Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := + match bi with + | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw + + | PLoadRRO n d a ofs => parexec_load (load_chunk n) rsr rsw mr mw d a ofs + + | PStoreRRO n s a ofs => exec_store ge (store_chunk n) rsr mr s a ofs + + | Pallocframe sz pos => + let (mw, stk) := Mem.alloc mr 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mptr mw (Val.offset_ptr sp pos) rsr#SP with + | None => Stuck + | Some mw => Next (rsw #FP <- (rsr SP) #SP <- sp #RTMP <- Vundef) mw + end + + | Pfreeframe sz pos => + match Mem.loadv Mptr mr (Val.offset_ptr rsr#SP pos) with + | None => Stuck + | Some v => + match rsr SP with + | Vptr stk ofs => + match Mem.free mr stk 0 sz with + | None => Stuck + | Some mw => Next (rsw#SP <- v #RTMP <- Vundef) mw + end + | _ => Stuck + end + end + | Pget rd ra => + match ra with + | RA => Next (rsw#rd <- (rsr#ra)) mw + | _ => Stuck + end + | Pset ra rd => + match ra with + | RA => Next (rsw#ra <- (rsr#rd)) mw + | _ => Stuck + end + | Pnop => Next rsw mw +end. + +(* parexec with writes-in-order *) +Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := + match body with + | nil => Next rsw mw + | bi::body' => + match parexec_basic_instr bi rsr rsw mr mw with + | Next rsw mw => parexec_wio_body body' rsr rsw mr mw + | Stuck => Stuck + end + end. + +(** Manipulations over the [PC] register: continuing with the next + instruction ([nextblock]) or branching to a label ([goto_label]). *) + +(* TODO: factoriser ? *) +Definition par_nextblock size_b (rsr rsw: regset) := + rsw#PC <- (Val.offset_ptr rsr#PC size_b). + +(* TODO: factoriser ? *) +Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := + match label_pos lbl 0 (fn_blocks f) with + | None => Stuck + | Some pos => + match rsr#PC with + | Vptr b ofs => Next (rsw#PC <- (Vptr b (Ptrofs.repr pos))) mw + | _ => Stuck + end + end. + +(** Evaluating a branch + +Warning: in m PC is assumed to be already pointing on the next instruction ! + +*) +(* TODO: factoriser ? *) +Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) := + match res with + | Some true => par_goto_label f l rsr rsw mw + | Some false => Next rsw mw + | None => Stuck + end. + + +(** Execution of a single control-flow instruction [i] in initial state [rs] and + [m]. Return updated state. + + As above: PC is assumed to be incremented on the next block before the control-flow instruction + + For instructions that correspond tobuiltin + actual RISC-V instructions, the cases are straightforward + transliterations of the informal descriptions given in the RISC-V + user-mode specification. For pseudo-instructions, refer to the + informal descriptions given above. + + Note that we set to [Vundef] the registers used as temporaries by + the expansions of the pseudo-instructions, so that the RISC-V code + we generate cannot use those registers to hold values that must + survive the execution of the pseudo-instruction. *) + +Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) (mw: mem) := + match oc with + | Some ic => +(** Get/Set system registers *) + match ic with + + +(** Branch Control Unit instructions *) + | Pret => + Next (rsw#PC <- (rsr#RA)) mw + | Pcall s => + Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw + | Picall r => + Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw + | Pgoto s => + Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw + | Pigoto r => + Next (rsw#PC <- (rsr#r)) mw + | Pj_l l => + par_goto_label f l rsr rsw mw + | Pcb bt r l => + match cmp_for_btest bt with + | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.cmp_bool c rsr#r (Vint (Int.repr 0))) + | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.cmpl_bool c rsr#r (Vlong (Int64.repr 0))) + | (None, _) => Stuck + end + | Pcbu bt r l => + match cmpu_for_btest bt with + | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0))) + | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0))) + | (None, _) => Stuck + end + + +(** Pseudo-instructions *) + | Pbuiltin ef args res => + Stuck (**r treated specially below *) + end + | None => Next rsw mw +end. + + +Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome := + match parexec_wio_body bdy rs rs m m with + | Next rsw mw => + let rsw := par_nextblock size_b rs rsw in + parexec_control f ext rs rsw mw + | Stuck => Stuck + end. + +(* utile ? *) +Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := + parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. + + +Require Import Sorting.Permutation. + +Inductive parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome -> Prop := + parexec_bblock_Next bdy1 bdy2 rsw mw: + Permutation (bdy1++bdy2) (body b) -> + parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rsw mw -> + parexec_bblock f b rs m (parexec_wio_body bdy2 rs rsw m mw) + | parexec_bblock_Stuck bdy1 bdy2: + Permutation (bdy1++bdy2) (body b) -> + parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> + parexec_bblock f b rs m Stuck. + + +Inductive step: state -> trace -> state -> Prop := + | exec_step_internal: + forall b ofs f bi rs m rs' m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi -> + exec_bblock ge f bi rs m = Next rs' m' -> + parexec_bblock f bi rs m (Next rs' m') -> + step (State rs m) E0 (State rs' m') + | exec_step_builtin: + forall b ofs f ef args res rs m vargs t vres rs' m' bi, + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) f.(fn_blocks) = Some bi -> + exit bi = Some (PExpand (Pbuiltin ef args res)) -> + eval_builtin_args ge rs (rs SP) m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = nextblock bi + (set_res res vres + (undef_regs (map preg_of (destroyed_by_builtin ef)) + (rs#RTMP <- Vundef))) -> + step (State rs m) t (State rs' m') + | exec_step_external: + forall b ef args res rs m t rs' m', + rs PC = Vptr b Ptrofs.zero -> + Genv.find_funct_ptr ge b = Some (External ef) -> + external_call ef ge args m t res m' -> + extcall_arguments rs m (ef_sig ef) args -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) -> + step (State rs m) t (State rs' m') + . + +End RELSEM. + +(** Execution of whole programs. *) + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +Lemma semantics_determinate: forall p, determinate (semantics p). +Proof. +Ltac Equalities := + match goal with + | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => + rewrite H1 in H2; inv H2; Equalities + | _ => idtac + end. + intros; constructor; simpl; intros. +- (* determ *) + inv H; inv H0; Equalities. + + split. constructor. auto. + + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate. + rewrite H10 in H4. discriminate. + + unfold exec_bblock in H14. (* FIXME: destruct (exec_body _ _ _ _); try discriminate. + rewrite H4 in H13. discriminate. + + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H6. eexact H13. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. +- (* trace length *) + red; intros. inv H; simpl. + omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +- (* initial states *) + inv H; inv H0. f_equal. congruence. +- (* final no step *) + assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs). + { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. } + inv H. unfold Vzero in H0. red; intros; red; intros. + inv H; rewrite H0 in *; eelim NOTNULL; eauto. +- (* final states *) + inv H; inv H0. congruence. *) +Admitted. \ No newline at end of file diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2de49faa..2e463f18 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -67,11 +67,10 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -Lemma next_eq {A: Type}: - forall (rs rs':A) m m', +Lemma next_eq rs rs' m m': rs = rs' -> m = m' -> Next rs m = Next rs' m'. Proof. - intros. congruence. + intros; apply f_equal2; auto. Qed. Lemma regset_double_set: @@ -659,8 +658,8 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. -Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). (* FIXME a remplacer par Asmvliw.semantics tprog *) Proof. eapply forward_simulation_plus. - apply senv_preserved. -- cgit From 2636b70dc48752ce21221c1fcf18c7a83086171d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 14 Mar 2019 21:45:18 +0100 Subject: fix the step_internal of Asmvliw - Actually, we want to show that the outcome is the same for any order of "writes" in the parallel execution. (ie we ask that bundles have a deterministic semantics for parallel execution) - we relax the condition that the outcome should be given for sequential execution instead, we ask that the it is given for the "in order" writes. In theory, the semantics would also accept bundles like "R1 := R2 R2 := R1" which are deterministic for parallel execution But, of course, in practice, we will also prove the sequential execution. --- mppa_k1c/Asmvliw.v | 42 +++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 2c88673b..5b58118b 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -233,23 +233,27 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: | Stuck => Stuck end. -(* utile ? *) Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. - Require Import Sorting.Permutation. -Inductive parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome -> Prop := - parexec_bblock_Next bdy1 bdy2 rsw mw: - Permutation (bdy1++bdy2) (body b) -> - parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rsw mw -> - parexec_bblock f b rs m (parexec_wio_body bdy2 rs rsw m mw) - | parexec_bblock_Stuck bdy1 bdy2: - Permutation (bdy1++bdy2) (body b) -> - parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck -> - parexec_bblock f b rs m Stuck. +Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop := + exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ + o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with + | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw + | Stuck => Stuck + end. +Lemma parexec_bblock_write_in_order f b rs m: + parexec_bblock f b rs m (parexec_wio_bblock f b rs m). +Proof. + exists (body b). exists nil. + constructor 1. + - rewrite app_nil_r; auto. + - unfold parexec_wio_bblock. + destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto. +Qed. Inductive step: state -> trace -> state -> Prop := | exec_step_internal: @@ -257,8 +261,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi -> - exec_bblock ge f bi rs m = Next rs' m' -> - parexec_bblock f bi rs m (Next rs' m') -> + parexec_wio_bblock f bi rs m = Next rs' m' -> + (forall o, parexec_bblock f bi rs m o -> o=(Next rs' m')) -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs f ef args res rs m vargs t vres rs' m' bi, @@ -301,11 +305,11 @@ Ltac Equalities := intros; constructor; simpl; intros. - (* determ *) inv H; inv H0; Equalities. - + split. constructor. auto. - + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate. + + split. constructor. auto. + + unfold parexec_wio_bblock, parexec_wio_bblock_aux in H4. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate. rewrite H10 in H4. discriminate. - + unfold exec_bblock in H14. (* FIXME: destruct (exec_body _ _ _ _); try discriminate. - rewrite H4 in H13. discriminate. + + unfold parexec_wio_bblock, parexec_wio_bblock_aux in H11. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate. + rewrite H4 in H11. discriminate. + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. exploit external_call_determ. eexact H6. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. @@ -325,5 +329,5 @@ Ltac Equalities := inv H. unfold Vzero in H0. red; intros; red; intros. inv H; rewrite H0 in *; eelim NOTNULL; eauto. - (* final states *) - inv H; inv H0. congruence. *) -Admitted. \ No newline at end of file + inv H; inv H0. congruence. +Qed. \ No newline at end of file -- cgit From 92188c18a3761fa14dfdb97010cebe919548a010 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 18 Mar 2019 12:06:57 +0100 Subject: Idée de preuve VLIW MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/PostpassSchedulingproof.v | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2e463f18..7d6d9a7a 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -658,8 +658,8 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. -Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). (* FIXME a remplacer par Asmvliw.semantics tprog *) +Theorem transf_program_correct_Asmblock: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). Proof. eapply forward_simulation_plus. - apply senv_preserved. @@ -668,4 +668,23 @@ Proof. - apply transf_step_correct. Qed. +(* TODO: +Require Import Asmvliw. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). +Proof. + eapply forward_simulation_one_one. (* FIXME *) +Admitted. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). +Proof. + eapply forward_simulation_compose. (* FIXME *) +Admitted. + +*) + + + End PRESERVATION. -- cgit From 6462da4e8f25ce5df951635828901ad0180e9958 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 20 Mar 2019 12:00:16 +0100 Subject: Integrating Asmvliw.v in the proof chain --- mppa_k1c/Asm.v | 6 +++--- mppa_k1c/Asmvliw.v | 5 ++--- mppa_k1c/PostpassSchedulingproof.v | 34 ++++++++++++++++++++++++---------- 3 files changed, 29 insertions(+), 16 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 31bc855d..0d4906b9 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -30,7 +30,7 @@ Require Import Smallstep. Require Import Locations. Require Stacklayout. Require Import Conventions. -Require Import Asmblock. +Require Import Asmvliw. Require Import Linking. Require Import Errors. @@ -416,7 +416,7 @@ Definition program_proj (p: program) : Asmblock.program := End RELSEM. -Definition semantics (p: program) := Asmblock.semantics (program_proj p). +Definition semantics (p: program) := Asmvliw.semantics (program_proj p). (** Determinacy of the [Asm] semantics. *) @@ -547,7 +547,7 @@ Proof (Genv.senv_match TRANSF). Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (semantics tprog). + forward_simulation (Asmvliw.semantics prog) (semantics tprog). Proof. pose proof (match_program_transf prog tprog TRANSF) as TR. subst. unfold semantics. rewrite transf_program_proj. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 5b58118b..36c68acd 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -31,7 +31,8 @@ Require Import Locations. Require Stacklayout. Require Import Conventions. Require Import Errors. -Require Import Asmblock. +Require Export Asmblock. +Require Import Sorting.Permutation. Local Open Scope asm. @@ -236,8 +237,6 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. -Require Import Sorting.Permutation. - Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop := exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 7d6d9a7a..6fff3117 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -237,7 +237,7 @@ Proof. rewrite <- Zplus_mod. auto. Qed. -Section PRESERVATION. +Section PRESERVATION_ASMBLOCK. Variables prog tprog: program. Hypothesis TRANSL: match_prog prog tprog. @@ -668,23 +668,37 @@ Proof. - apply transf_step_correct. Qed. -(* TODO: +End PRESERVATION_ASMBLOCK. + Require Import Asmvliw. -Theorem transf_program_correct: +Section PRESERVATION_ASMVLIW. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Theorem transf_program_correct_Asmvliw: forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). Proof. - eapply forward_simulation_one_one. (* FIXME *) Admitted. -Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). -Proof. - eapply forward_simulation_compose. (* FIXME *) -Admitted. +End PRESERVATION_ASMVLIW. -*) +Section PRESERVATION. +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). +Proof. + eapply compose_forward_simulations. + eapply transf_program_correct_Asmblock; eauto. + eapply transf_program_correct_Asmvliw; eauto. +Qed. End PRESERVATION. -- cgit From e25099690ddfc45579c318940f3304ab6400135c Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 20 Mar 2019 17:50:16 +0100 Subject: premier decoupage --- mppa_k1c/PostpassSchedulingproof.v | 58 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 2 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 6fff3117..25bdf244 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -670,7 +670,7 @@ Qed. End PRESERVATION_ASMBLOCK. -Require Import Asmvliw. +Require Import Asmvliw List. Section PRESERVATION_ASMVLIW. @@ -679,10 +679,64 @@ Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. + +Lemma transf_blocks_checks_all_bundles lbb bundles: + transf_blocks (lbb : list bblock) = OK bundles -> + List.Forall (fun bb => verify_par_bblock bb = OK tt) bundles. +Proof. +Admitted. + +Lemma all_bundles_are_checked b ofs f bundle: + Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> + verify_par_bblock bundle = OK tt. +Proof. + unfold match_prog, match_program, match_program_gen in TRANSL. + (* HOW CAN WE PROVE THIS FROM transf_blocks_checks_all_bundles ?? *) +Admitted. + +Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: + exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> + verify_par_bblock bundle = OK tt -> + parexec_bblock (globalenv (semantics tprog)) f bundle rs m o -> o = Next rs' m'. +Proof. +Admitted. + +Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m' o: + (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) + Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> + exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> + parexec_bblock (globalenv (semantics tprog)) f bundle rs m o -> o = Next rs' m'. +Proof. + intros; eapply checked_bundles_are_parexec_equiv; eauto. + eapply all_bundles_are_checked; eauto. +Qed. + +Lemma seqexec_parexec_wio b ofs f bundle rs rs' m m': + (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) + Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> + exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> + parexec_wio_bblock (globalenv (semantics tprog)) f bundle rs m = Next rs' m'. +Proof. + intros; erewrite <- seqexec_parexec_equiv; eauto. + eapply parexec_bblock_write_in_order. +Qed. + + Theorem transf_program_correct_Asmvliw: forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). Proof. -Admitted. + eapply forward_simulation_step with (match_states:=fun (s1:Asmblock.state) s2 => s1=s2); eauto. + - intros; subst; auto. + - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto. + + eapply exec_step_internal; eauto. + eapply seqexec_parexec_wio; eauto. + intros; eapply seqexec_parexec_equiv; eauto. + + eapply exec_step_builtin; eauto. + + eapply exec_step_external; eauto. +Qed. End PRESERVATION_ASMVLIW. -- cgit From 4d5b986ff72098466b3a3bb02c20d0ca697243da Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 20 Mar 2019 19:56:42 +0100 Subject: one step further... --- mppa_k1c/PostpassSchedulingproof.v | 34 ++++++++++++++++++++++++++++------ 1 file changed, 28 insertions(+), 6 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 25bdf244..5b3768af 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -680,9 +680,9 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Lemma transf_blocks_checks_all_bundles lbb bundles: - transf_blocks (lbb : list bblock) = OK bundles -> - List.Forall (fun bb => verify_par_bblock bb = OK tt) bundles. +Lemma transf_blocks_checks_all_bundles ofs lbb lb bundle: + transf_blocks lbb = OK lb -> + find_bblock (Ptrofs.unsigned ofs) lb = Some bundle -> verify_par_bblock bundle = OK tt. Proof. Admitted. @@ -691,9 +691,31 @@ Lemma all_bundles_are_checked b ofs f bundle: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> verify_par_bblock bundle = OK tt. Proof. - unfold match_prog, match_program, match_program_gen in TRANSL. - (* HOW CAN WE PROVE THIS FROM transf_blocks_checks_all_bundles ?? *) -Admitted. + unfold match_prog, match_program in TRANSL. + unfold Genv.find_funct_ptr; simpl; intros X. + destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence. + destruct y as [tf0|]; try congruence. + inversion X as [H1]. subst. clear X. + remember (@Gfun fundef unit (Internal f)) as f2. + destruct H as [ctx' f1 f2 H0|]; try congruence. + inversion Heqf2 as [H2]. subst; clear Heqf2. + unfold transf_fundef, transf_partial_fundef in H. + (* TODO: is there any way to simplify these reasonings in the monad ? *) + destruct f1 as [f1|f1]; try congruence. + remember (transf_function f1) as tf1. + destruct tf1 as [f0|]; simpl in *|-; try congruence. + inversion H as [H1]. subst. clear H. + unfold transf_function in Heqtf1. + remember (transl_function f1) as tf0. + destruct tf0 as [f0|]; simpl in *|-; try congruence. + destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks f0))); simpl in *|-; try congruence. + inversion Heqtf1 as [H]. subst; clear Heqtf1. + unfold transl_function in Heqtf0. + remember (transf_blocks (fn_blocks f1)) as olb. + destruct olb as [lb|]; simpl in *|-; try congruence. + inversion Heqtf0 as [H]. subst; clear Heqtf0. simpl. + intros; exploit transf_blocks_checks_all_bundles; eauto. +Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> -- cgit From 0dcfa3fef12bcf0185b75c089aa811441c2ea83c Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 20 Mar 2019 21:06:43 +0100 Subject: yet another step backward --- mppa_k1c/PostpassSchedulingproof.v | 57 ++++++++++++++++++++++++++------------ 1 file changed, 39 insertions(+), 18 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 5b3768af..4cd40716 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -670,6 +670,9 @@ Qed. End PRESERVATION_ASMBLOCK. + + + Require Import Asmvliw List. Section PRESERVATION_ASMVLIW. @@ -679,16 +682,38 @@ Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Lemma find_bblock_split lb1: forall ofs lb2 bundle, + find_bblock ofs (lb1 ++ lb2) = Some bundle -> + find_bblock ofs lb1 = Some bundle \/ (exists ofs', find_bblock ofs' lb2 = Some bundle). +Proof. + induction lb1; simpl; eauto. + intros ofs lbd2 bundle H. + destruct (zlt ofs 0); eauto. + destruct (zeq ofs 0); eauto. +Qed. -Lemma transf_blocks_checks_all_bundles ofs lbb lb bundle: - transf_blocks lbb = OK lb -> - find_bblock (Ptrofs.unsigned ofs) lb = Some bundle -> verify_par_bblock bundle = OK tt. +Lemma verified_schedule_checks_alls_bundles bb: forall ofs lb bundle, + verified_schedule bb = OK lb -> + find_bblock ofs lb = Some bundle -> + verify_par_bblock bundle = OK tt. Proof. Admitted. +Lemma transf_blocks_checks_all_bundles lbb: forall ofs lb bundle, + transf_blocks lbb = OK lb -> + find_bblock ofs lb = Some bundle -> verify_par_bblock bundle = OK tt. +Proof. + induction lbb; simpl. + - intros ofs lb bundle H; inversion_clear H. simpl; try congruence. + - intros ofs lb bundle H0. + monadInv H0. + intros H; destruct (find_bblock_split _ _ _ _ H) as [|(ofs' & Hofs')]; eauto. + eapply verified_schedule_checks_alls_bundles; eauto. +Qed. + Lemma all_bundles_are_checked b ofs f bundle: Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> - find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> + find_bblock ofs (fn_blocks f) = Some bundle -> verify_par_bblock bundle = OK tt. Proof. unfold match_prog, match_program in TRANSL. @@ -700,21 +725,14 @@ Proof. destruct H as [ctx' f1 f2 H0|]; try congruence. inversion Heqf2 as [H2]. subst; clear Heqf2. unfold transf_fundef, transf_partial_fundef in H. - (* TODO: is there any way to simplify these reasonings in the monad ? *) destruct f1 as [f1|f1]; try congruence. - remember (transf_function f1) as tf1. - destruct tf1 as [f0|]; simpl in *|-; try congruence. - inversion H as [H1]. subst. clear H. - unfold transf_function in Heqtf1. - remember (transl_function f1) as tf0. - destruct tf0 as [f0|]; simpl in *|-; try congruence. - destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks f0))); simpl in *|-; try congruence. - inversion Heqtf1 as [H]. subst; clear Heqtf1. - unfold transl_function in Heqtf0. - remember (transf_blocks (fn_blocks f1)) as olb. - destruct olb as [lb|]; simpl in *|-; try congruence. - inversion Heqtf0 as [H]. subst; clear Heqtf0. simpl. - intros; exploit transf_blocks_checks_all_bundles; eauto. + monadInv H. unfold transf_function in EQ. + monadInv EQ. + destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence. + injection EQ1; intros; subst. + unfold transl_function in EQ0. + monadInv EQ0. simpl in * |-. + exploit transf_blocks_checks_all_bundles; eauto. Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: @@ -762,6 +780,9 @@ Qed. End PRESERVATION_ASMVLIW. + + + Section PRESERVATION. Variables prog tprog: program. -- cgit From ad69926edbee2832242d0b991a654cbda66ff367 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 21 Mar 2019 07:10:14 +0100 Subject: simplification of the proof --- mppa_k1c/PostpassScheduling.v | 7 +-- mppa_k1c/PostpassSchedulingproof.v | 92 +++++++++++++++++++++++++++----------- 2 files changed, 70 insertions(+), 29 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index b5d55ad3..8cc74eda 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -351,8 +351,9 @@ Definition verified_schedule_nob (bb : bblock) : res (list bblock) := do tbb <- concat_all lbb; do sizecheck <- verify_size bb lbb; do schedcheck <- verify_schedule bb' tbb; - do parcheck <- verify_par lbb; - stick_header_code (header bb) lbb. + do res <- stick_header_code (header bb) lbb; + do parcheck <- verify_par res; + OK res. Lemma verified_schedule_nob_size: forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb. @@ -378,7 +379,7 @@ Lemma verified_schedule_nob_header: /\ Forall (fun b => header b = nil) lbb. Proof. intros. split. - - monadInv H. unfold stick_header_code in EQ4. destruct (hd_error _); try discriminate. inv EQ4. + - monadInv H. unfold stick_header_code in EQ2. destruct (hd_error _); try discriminate. inv EQ2. simpl. reflexivity. - apply verified_schedule_nob_no_header_in_middle in H. assumption. Qed. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 4cd40716..1fc5c506 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -673,44 +673,84 @@ End PRESERVATION_ASMBLOCK. -Require Import Asmvliw List. +Require Import Asmvliw. -Section PRESERVATION_ASMVLIW. -Variables prog tprog: program. -Hypothesis TRANSL: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. +Lemma verified_par_checks_alls_bundles lb x: forall bundle, + verify_par lb = OK x -> + List.In bundle lb -> verify_par_bblock bundle = OK tt. +Proof. + induction lb; simpl; try tauto. + intros bundle H; monadInv H. + destruct 1; subst; eauto. + destruct x0; auto. +Qed. -Lemma find_bblock_split lb1: forall ofs lb2 bundle, - find_bblock ofs (lb1 ++ lb2) = Some bundle -> - find_bblock ofs lb1 = Some bundle \/ (exists ofs', find_bblock ofs' lb2 = Some bundle). + +Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle: + verified_schedule_nob bb = OK lb -> + List.In bundle lb -> verify_par_bblock bundle = OK tt. Proof. - induction lb1; simpl; eauto. - intros ofs lbd2 bundle H. - destruct (zlt ofs 0); eauto. - destruct (zeq ofs 0); eauto. + unfold verified_schedule_nob. intros H; + monadInv H. destruct x3. + intros; eapply verified_par_checks_alls_bundles; eauto. +Qed. + +Lemma verify_par_bblock_PExpand bb i: + exit bb = Some (PExpand i) -> verify_par_bblock bb = OK tt. +Proof. + destruct bb as [h bdy ext H]; simpl. + intros; subst. destruct i. + generalize H. + rewrite <- AB.wf_bblock_refl in H. + destruct H as [H H0]. + unfold AB.builtin_alone in H0. erewrite H0; eauto. Qed. -Lemma verified_schedule_checks_alls_bundles bb: forall ofs lb bundle, +Local Hint Resolve verified_schedule_nob_checks_alls_bundles. + +Lemma verified_schedule_checks_alls_bundles bb lb bundle: verified_schedule bb = OK lb -> - find_bblock ofs lb = Some bundle -> - verify_par_bblock bundle = OK tt. + List.In bundle lb -> verify_par_bblock bundle = OK tt. Proof. -Admitted. + unfold verified_schedule. remember (exit bb) as exb. + destruct exb as [c|]; eauto. + destruct c as [i|]; eauto. + destruct i; intros H. inversion_clear H; simpl. + intuition subst. + intros; eapply verify_par_bblock_PExpand; eauto. +Qed. -Lemma transf_blocks_checks_all_bundles lbb: forall ofs lb bundle, +Lemma transf_blocks_checks_all_bundles lbb: forall lb bundle, transf_blocks lbb = OK lb -> - find_bblock ofs lb = Some bundle -> verify_par_bblock bundle = OK tt. + List.In bundle lb -> verify_par_bblock bundle = OK tt. Proof. induction lbb; simpl. - - intros ofs lb bundle H; inversion_clear H. simpl; try congruence. - - intros ofs lb bundle H0. + - intros lb bundle H; inversion_clear H. simpl; try tauto. + - intros lb bundle H0. monadInv H0. - intros H; destruct (find_bblock_split _ _ _ _ H) as [|(ofs' & Hofs')]; eauto. + rewrite in_app. destruct 1; eauto. eapply verified_schedule_checks_alls_bundles; eauto. Qed. +Lemma find_bblock_forall_inv lb P: + (forall b, List.In b lb -> P b) -> + forall ofs b, find_bblock ofs lb = Some b -> P b. +Proof. + induction lb; simpl; try congruence. + intros H ofs b. + destruct (zlt ofs 0); try congruence. + destruct (zeq ofs 0); eauto. + intros X; inversion X; eauto. +Qed. + +Section PRESERVATION_ASMVLIW. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + Lemma all_bundles_are_checked b ofs f bundle: Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> find_bblock ofs (fn_blocks f) = Some bundle -> @@ -726,13 +766,13 @@ Proof. inversion Heqf2 as [H2]. subst; clear Heqf2. unfold transf_fundef, transf_partial_fundef in H. destruct f1 as [f1|f1]; try congruence. - monadInv H. unfold transf_function in EQ. - monadInv EQ. + unfold transf_function, transl_function in H. + monadInv H. monadInv EQ. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence. injection EQ1; intros; subst. - unfold transl_function in EQ0. monadInv EQ0. simpl in * |-. - exploit transf_blocks_checks_all_bundles; eauto. + intros; pattern bundle; eapply find_bblock_forall_inv; eauto. + intros; exploit transf_blocks_checks_all_bundles; eauto. Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: -- cgit 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 ++++++++++++++++++++++++++++++++++++++ mppa_k1c/PostpassSchedulingproof.v | 5 ++- 2 files changed, 72 insertions(+), 1 deletion(-) (limited to 'mppa_k1c') 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. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 1fc5c506..57a84480 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -780,7 +780,10 @@ Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: verify_par_bblock bundle = OK tt -> parexec_bblock (globalenv (semantics tprog)) f bundle rs m o -> o = Next rs' m'. Proof. -Admitted. + intros. unfold verify_par_bblock in H0. destruct (Asmblockdeps.bblock_para_check _) eqn:BPC; try discriminate. clear H0. + simpl in H. simpl in H1. + eapply Asmblockdeps.bblock_para_check_correct; eauto. +Qed. Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m' o: (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) -- 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 +++-- mppa_k1c/PostpassSchedulingproof.v | 2 -- 2 files changed, 3 insertions(+), 4 deletions(-) (limited to 'mppa_k1c') 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. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 57a84480..f5a84db7 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -786,7 +786,6 @@ Proof. Qed. Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m' o: - (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> @@ -797,7 +796,6 @@ Proof. Qed. Lemma seqexec_parexec_wio b ofs f bundle rs rs' m m': - (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> -- 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') 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 313db9c2b0b69fbbb2005ed90fd221932f87e5a0 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 23 Mar 2019 08:00:52 +0100 Subject: slight simplification --- mppa_k1c/PostpassSchedulingproof.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f5a84db7..634f50bb 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -733,12 +733,11 @@ Proof. eapply verified_schedule_checks_alls_bundles; eauto. Qed. -Lemma find_bblock_forall_inv lb P: - (forall b, List.In b lb -> P b) -> - forall ofs b, find_bblock ofs lb = Some b -> P b. +Lemma find_bblock_Some_in lb: + forall ofs b, find_bblock ofs lb = Some b -> List.In b lb. Proof. induction lb; simpl; try congruence. - intros H ofs b. + intros ofs b. destruct (zlt ofs 0); try congruence. destruct (zeq ofs 0); eauto. intros X; inversion X; eauto. @@ -771,8 +770,8 @@ Proof. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence. injection EQ1; intros; subst. monadInv EQ0. simpl in * |-. - intros; pattern bundle; eapply find_bblock_forall_inv; eauto. intros; exploit transf_blocks_checks_all_bundles; eauto. + intros; eapply find_bblock_Some_in; eauto. Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: -- 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 +++++++++++++++++++++++++++++++++++++++++++++++- mppa_k1c/Asmvliw.v | 15 ++- 2 files changed, 287 insertions(+), 4 deletions(-) (limited to 'mppa_k1c') 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) -> diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 36c68acd..0490e502 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -78,6 +78,17 @@ Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) | _ => Stuck end. +Definition parexec_store (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) + (s: ireg) (a: ireg) (ofs: offset) := + match (eval_offset ge ofs) with + | OK ptr => + match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' + end + | _ => Stuck + end. + (* rem: parexec_store = exec_store *) (** * basic instructions *) @@ -89,7 +100,7 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := | PLoadRRO n d a ofs => parexec_load (load_chunk n) rsr rsw mr mw d a ofs - | PStoreRRO n s a ofs => exec_store ge (store_chunk n) rsr mr s a ofs + | PStoreRRO n s a ofs => parexec_store (store_chunk n) rsr rsw mr mw s a ofs | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in @@ -163,7 +174,7 @@ Warning: in m PC is assumed to be already pointing on the next instruction ! Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) := match res with | Some true => par_goto_label f l rsr rsw mw - | Some false => Next rsw mw + | Some false => Next (rsw # PC <- (rsr PC)) mw | None => Stuck end. -- 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') 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 +++++++++++++++++++++++++++--------------------- mppa_k1c/Asmvliw.v | 7 +- 2 files changed, 113 insertions(+), 91 deletions(-) (limited to 'mppa_k1c') 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. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 0490e502..d3349344 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -151,8 +151,8 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := instruction ([nextblock]) or branching to a label ([goto_label]). *) (* TODO: factoriser ? *) -Definition par_nextblock size_b (rsr rsw: regset) := - rsw#PC <- (Val.offset_ptr rsr#PC size_b). +Definition par_nextblock size_b (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC size_b). (* TODO: factoriser ? *) Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := @@ -240,7 +240,8 @@ end. Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome := match parexec_wio_body bdy rs rs m m with | Next rsw mw => - let rsw := par_nextblock size_b rs rsw in + let rs := par_nextblock size_b rs in + let rsw := par_nextblock size_b rsw in parexec_control f ext rs rsw mw | Stuck => Stuck end. -- 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 ++++++++++++++++++++++++++---------------------- mppa_k1c/Asmvliw.v | 14 +++--- 2 files changed, 70 insertions(+), 60 deletions(-) (limited to 'mppa_k1c') 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. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index d3349344..8407f28d 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -233,25 +233,25 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) | Pbuiltin ef args res => Stuck (**r treated specially below *) end - | None => Next rsw mw + | None => Next (rsw#PC <- (rsr#PC)) mw end. -Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome := - match parexec_wio_body bdy rs rs m m with +Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome := + match parexec_wio_body bdy rsr rsw mr mw with | Next rsw mw => - let rs := par_nextblock size_b rs in + let rsr := par_nextblock size_b rsr in let rsw := par_nextblock size_b rsw in - parexec_control f ext rs rsw mw + parexec_control f ext rsr rsw mw | Stuck => Stuck end. Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := - parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. + parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m. Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop := exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ - o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with + o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs rs m m with | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw | Stuck => Stuck end. -- 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') 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 +++++++++++++++++++++++--------- mppa_k1c/abstractbb/Parallelizability.v | 18 ++++++ 2 files changed, 100 insertions(+), 29 deletions(-) (limited to 'mppa_k1c') 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: diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index b6d1f142..065c0922 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -79,6 +79,24 @@ Proof. + intros H1; rewrite H1; simpl; auto. Qed. +Lemma prun_iw_app_None p1: forall m1 old p2, + prun_iw p1 m1 old = None -> + prun_iw (p1++p2) m1 old = None. +Proof. + induction p1; simpl; try congruence. + intros; destruct (macro_prun _ _ _); simpl; auto. +Qed. + +Lemma prun_iw_app_Some p1: forall m1 old m2 p2, + prun_iw p1 m1 old = Some m2 -> + prun_iw (p1++p2) m1 old = prun_iw p2 m2 old. +Proof. + induction p1; simpl; try congruence. + intros; destruct (macro_prun _ _ _); simpl; auto. + congruence. +Qed. + + End PARALLEL. End ParallelSemantics. -- cgit