From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Jul 2021 18:25:00 +0200 Subject: non trapping loads --- scheduling/BTL.v | 51 ++++++++++++++++++++++++++++++----------- scheduling/BTL_Livecheck.v | 14 ++++++----- scheduling/BTL_SEimpl.v | 15 +++++------- scheduling/BTL_SEsimuref.v | 9 +++----- scheduling/BTL_SEtheory.v | 44 +++++++++++++++++++++-------------- scheduling/BTL_Schedulerproof.v | 2 +- scheduling/BTLmatchRTL.v | 14 +++++++---- scheduling/BTLtoRTLproof.v | 3 ++- scheduling/RTLtoBTLproof.v | 15 +++++++----- 9 files changed, 103 insertions(+), 64 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 6536addb..96377943 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -205,7 +205,7 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef := Local Open Scope option_monad_scope. -(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) +(* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := | has_loaded_normal a trap @@ -217,11 +217,10 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (DEFAULT: v = default_notrap_load_value chunk) : has_loaded sp rs m chunk addr args v NOTRAP . +Local Hint Constructors has_loaded: core. (* TODO: move this scheme in "Memory" module if this scheme is useful ! *) -*) - (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) @@ -229,15 +228,9 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v iinfo - (EVAL: eval_addressing ge sp addr rs##args = Some a) - (LOAD: Mem.loadv chunk m a = Some v) - : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None -(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above - | exec_load rs m trap chunk addr args dst v + | exec_load rs m trap chunk addr args dst v iinfo (LOAD: has_loaded sp rs m chunk addr args v trap) - : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None -*) + : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (rs#dst <- v) m None | exec_store rs m chunk addr args src a m' iinfo (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') @@ -274,7 +267,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := SOME v <- Mem.loadv chunk m a IN Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} | Bload NOTRAP chunk addr args dst _ => - None (* TODO *) + match eval_addressing ge sp addr rs##args with + | Some a => + match Mem.loadv chunk m a with + | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end | Bstore chunk addr args src _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME m' <- Mem.storev chunk m a rs#src IN @@ -291,13 +295,34 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := iblock_istep_run sp (if b then ifso else ifnot) rs m end. +Lemma iblock_istep_run_equiv_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin: + ib = (Bload trap chunk addr args dst iinfo) -> + rs' = rs # dst <- v -> + has_loaded sp rs m chunk addr args v trap -> + iblock_istep sp rs m ib rs' m ofin <-> + iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}. +Proof. + split; subst; inv H1; simpl in *; intros. + - destruct trap; inv H; simpl in *; repeat autodestruct. + - inv H; autodestruct; rewrite LOAD; auto. + - destruct trap; inv H; simpl in *; + rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto. + - generalize H; autodestruct. + + rewrite LOAD in *; inv H; auto; constructor. + eapply has_loaded_default; eauto; try_simplify_someHyps. + + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps. +Qed. +Local Hint Resolve iblock_istep_run_equiv_load: core. + Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin: iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}. Proof. constructor. - - induction 1; simpl; try autodestruct; try_simplify_someHyps. + - induction 1; try (eapply iblock_istep_run_equiv_load; eauto; fail); + simpl; try autodestruct; try_simplify_someHyps. - generalize rs m rs' m' ofin; clear rs m rs' m' ofin. induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps). + 1,2: constructor; eapply has_loaded_default; try_simplify_someHyps. destruct o; try_simplify_someHyps; subst; eauto. Qed. diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 9f96e74e..d200b9bd 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -546,12 +546,14 @@ Proof. - (* Bload *) erewrite <- eqlive_reg_listmem; eauto. try_simplify_someHyps; intros. - rewrite LOAD; eauto. - repeat econstructor. - apply eqlive_reg_update. - eapply eqlive_reg_monotonic; eauto. - intros r0; rewrite regset_add_spec. - intuition. + destruct trap; inv LOAD; + rewrite EVAL, LOAD0 || (autodestruct; try rewrite LOAD0; auto). + all: + repeat econstructor; + apply eqlive_reg_update; + eapply eqlive_reg_monotonic; eauto; + intros r0; rewrite regset_add_spec; + intuition. - (* Bstore *) erewrite <- eqlive_reg_listmem; eauto. rewrite <- (REGS src); auto. diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 305c3cfa..aa27bd19 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -823,11 +823,11 @@ Proof. simpl in *; econstructor; eauto. Qed. -Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs: - WHEN hrs_sreg_set dest args (Rload TRAP chunk addr) hrs ~> rst THEN +Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs trap: + WHEN hrs_sreg_set dest args (Rload trap chunk addr) hrs ~> rst THEN ris_ok ctx rst -> ris_ok ctx hrs. Proof. - wlp_simplify; inv H1; + wlp_simplify; inv H2 || inv H1; simpl in *; econstructor; eauto. Qed. @@ -1071,10 +1071,9 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := | Bop op args dst _ => DO next <~ hrs_sreg_set dst args (Rop op) hrs;; k next - | Bload TRAP chunk addr args dst _ => - DO next <~ hrs_sreg_set dst args (Rload TRAP chunk addr) hrs;; + | Bload trap chunk addr args dst _ => + DO next <~ hrs_sreg_set dst args (Rload trap chunk addr) hrs;; k next - | Bload NOTRAP chunk addr args dst _ => RET Rabort | Bstore chunk addr args src _ => DO next <~ hrexec_store chunk addr args src hrs;; k next @@ -1122,7 +1121,6 @@ Proof. intros X; apply H0 in X. exploit hrexec_final_sfv_correct; eauto. - (* Bnop *) wlp_simplify; eapply CONT; eauto. - - (* Bload *) destruct trap; wlp_simplify. - (* Bseq *) wlp_simplify. eapply IHib1. 3-7: eauto. @@ -1171,7 +1169,7 @@ Proof. - (* Bop *) wlp_simplify; exploit hrs_ok_op_okpreserv; eauto. - (* Bload *) - destruct trap; wlp_simplify; try_simplify_someHyps. + destruct trap; wlp_simplify; try_simplify_someHyps; exploit hrs_ok_load_okpreserv; eauto. - (* Bstore *) wlp_simplify; exploit hrs_ok_store_okpreserv; eauto. @@ -1207,7 +1205,6 @@ Proof. intros X; apply H0 in X. exploit hrexec_final_sfv_correct; eauto. - (* Bnop *) wlp_simplify; eapply CONT; eauto. - - (* Bload *) destruct trap; wlp_simplify. - (* Bseq *) wlp_simplify. eapply IHib1. 3-6: eauto. diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 7af1af62..d47e53b8 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -348,7 +348,7 @@ Proof. unfold sexec_op. rewrite ok_set_sreg. intuition. Qed. -Lemma si_ok_load_okpreserv ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. +Lemma si_ok_load_okpreserv ctx chunk addr args dest sis trap: si_ok ctx (sexec_load trap chunk addr args dest sis) -> si_ok ctx sis. Proof. unfold sexec_load. rewrite ok_set_sreg. intuition. Qed. @@ -705,8 +705,7 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := (* basic instructions *) | Bnop _ => k ris | Bop op args res _ => k (rexec_op op args res ris) - | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris) - | Bload NOTRAP chunk addr args dst _ => Rabort + | Bload trap chunk addr args dst _ => k (rexec_load trap chunk addr args dst ris) | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris) (* composed instructions *) | Bseq ib1 ib2 => @@ -739,7 +738,6 @@ Lemma rexec_rec_correct1 ctx ib: , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. Proof. induction ib; simpl; try (intros; subst; eauto; fail). - - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. @@ -774,7 +772,7 @@ Proof. unfold rexec_op. rewrite ok_rset_sreg. intuition. Qed. -Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. +Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris trap: ris_ok ctx (rexec_load trap chunk addr args dest ris) -> ris_ok ctx ris. Proof. unfold rexec_load. rewrite ok_rset_sreg. intuition. Qed. @@ -818,7 +816,6 @@ Lemma rexec_rec_correct2 ctx ib: , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). Proof. induction ib; simpl; try (intros; subst; eauto; fail). - - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 2a335790..e2e6be6b 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -626,18 +626,22 @@ Definition sexec_load trap chunk addr args dst sis: sistate := let args := list_sval_inj (List.map sis.(si_sreg) args) in set_sreg dst (fSload sis.(si_smem) trap chunk addr args) sis. -Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v - (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) - (LOAD: Mem.loadv chunk m a = Some v) +Lemma sexec_load_correct ctx chunk addr args dst sis rs m v trap + (HLOAD: has_loaded (cge ctx) (csp ctx) rs m chunk addr args v trap) (SIS: sem_sistate ctx sis rs m) - :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m). + :(sem_sistate ctx (sexec_load trap chunk addr args dst sis) (rs#dst <- v) m). Proof. - eapply set_sreg_correct; eauto. + inv HLOAD; eapply set_sreg_correct; eauto. + 2,4: intros; rewrite Regmap.gso; auto. + - simpl. destruct SIS as (PRE&MEM®). + destruct trap; rewrite Regmap.gss; simpl; auto; + erewrite eval_list_sval_inj; simpl; auto; + try_simplify_someHyps. + intros. rewrite LOAD; auto. - simpl. destruct SIS as (PRE&MEM®). rewrite Regmap.gss; simpl; auto. erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - - intros; rewrite Regmap.gso; auto. + autodestruct; rewrite MEM, LOAD; auto. Qed. Definition sexec_store chunk addr args src sis: sistate := @@ -812,8 +816,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := (* basic instructions *) | Bnop _ => k sis | Bop op args res _ => k (sexec_op op args res sis) - | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis) - | Bload NOTRAP chunk addr args dst _ => Sabort (* TODO *) + | Bload trap chunk addr args dst _ => k (sexec_load trap chunk addr args dst sis) | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis) (* composed instructions *) | Bseq ib1 ib2 => @@ -830,7 +833,7 @@ Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort). Local Hint Constructors sem_sstate: core. Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct - sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. + sexec_load_correct sexec_store_correct sis_init_correct: core. Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k @@ -921,9 +924,9 @@ Proof. intros; eapply set_sreg_preserves_abort; eauto. Qed. -Lemma sexec_load_preserves_abort ctx chunk addr args dest sis: +Lemma sexec_load_preserves_abort ctx chunk addr args dest sis trap: abort_sistate ctx sis - -> abort_sistate ctx (sexec_load TRAP chunk addr args dest sis). + -> abort_sistate ctx (sexec_load trap chunk addr args dest sis). Proof. intros; eapply set_sreg_preserves_abort; eauto. Qed. @@ -962,8 +965,6 @@ Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k Proof. induction ib; simpl; intros; eauto. - (* final *) inversion SEXEC; subst; eauto. - - (* load *) destruct trap; eauto. - inversion SEXEC. - (* seq *) eapply IHib1; eauto. simpl. eauto. @@ -1052,11 +1053,20 @@ Proof. * intros; rewrite REG, str_tr_regs_equiv; auto. * intros (s2 & EQUIV & SFV'); eauto. - (* Bop *) autodestruct; eauto. - - destruct trap; [| inv SEXEC ]. - repeat autodestruct; eauto. - all: intros; eapply CONT; eauto; + - destruct trap. + + repeat autodestruct. + { eexists; split; eauto. + eapply sexec_load_correct; eauto. + econstructor; eauto. } + all: + intros; eapply CONT; eauto; eapply sexec_load_TRAP_abort; eauto; intros; try_simplify_someHyps. + + repeat autodestruct; + eexists; split; eauto; + eapply sexec_load_correct; eauto; + try (econstructor; eauto; fail). + all: eapply has_loaded_default; auto; try_simplify_someHyps. - repeat autodestruct; eauto. all: intros; eapply CONT; eauto; eapply sexec_store_abort; eauto; diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 27efe56f..40ad0d88 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -354,7 +354,7 @@ Proof. - repeat econstructor; eauto. - repeat econstructor; eauto. erewrite args_eqregs; eauto. - - repeat econstructor; eauto. + - inv LOAD; repeat econstructor; eauto; erewrite args_eqregs; eauto. - repeat econstructor; eauto. erewrite args_eqregs; eauto. diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index a59c847e..c271ae02 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -48,11 +48,15 @@ Proof. do 2 eexists; rewrite EVAL'. repeat (split; eauto). eapply set_reg_lessdef; eauto. - (* Bload *) - exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. - intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. - intros (v3 & LOAD' & LESSDEF'). - do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto). - eapply set_reg_lessdef; eauto. + inv LOAD. + + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. + intros (v3 & LOAD' & LESSDEF'); autodestruct; + do 2 eexists; rewrite EVAL', LOAD'; + repeat (split; eauto); eapply set_reg_lessdef; eauto. + + destruct (eval_addressing ge sp addr rs ## args) eqn:EQA; + repeat autodestruct; do 2 eexists; + repeat (split; eauto); eapply set_reg_lessdef; eauto. - (* Bstore *) exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto. diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b8dabab..324f1d14 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -230,7 +230,8 @@ Proof. intros; rewrite symbols_preserved; trivial. - (* exec_load *) inv MIB. exists pc'; split; auto; constructor. - apply plus_one. eapply exec_Iload; eauto. + apply plus_one. inv LOAD. + eapply exec_Iload; eauto. all: erewrite <- eval_addressing_preserved; eauto; intros; rewrite symbols_preserved; trivial. - (* exec_store *) diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 8a352434..13ba5a29 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -123,12 +123,15 @@ Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1: iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2. Proof. induction 1; simpl; intuition subst; eauto. - { (* Bnop *) autodestruct; eauto. } - 1-3: (* Bop, Bload, Bstore *) - intros; repeat econstructor; eauto. - (* Bcond *) - destruct ofin; intuition subst; - destruct b; eapply IHISTEP; eauto. + - (* Bnop *) autodestruct; eauto. + - (* Bop *) repeat econstructor; eauto. + - (* Bload *) inv LOAD. + + repeat econstructor; eauto. + + do 2 (econstructor; eauto). + eapply has_loaded_default; eauto. + - (* Bcond *) repeat econstructor; eauto. + destruct ofin; intuition subst; + destruct b; eapply IHISTEP; eauto. Qed. Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: -- cgit