From d8cf80248c6aee35aff49ee8d4ca9d1c8fc906f5 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 7 Jul 2021 11:41:04 +0200 Subject: hrexec1 --- scheduling/BTL_SEimpl.v | 108 ++++++++++++++++++++++++++++++++++++------------ 1 file changed, 81 insertions(+), 27 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 94d7375d..c32001d4 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -670,15 +670,15 @@ Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := | None => FAILWITH msg end. -Definition hris_init: ?? ristate +Definition hrs_init: ?? ristate := DO hm <~ hSinit ();; RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. -Lemma ris_init_correct: - WHEN hris_init ~> hris THEN - forall ctx, ris_refines ctx hris sis_init. +Lemma hrs_init_correct: + WHEN hrs_init ~> hrs THEN + forall ctx, ris_refines ctx hrs sis_init. Proof. - unfold hris_init, sis_init; wlp_simplify. + unfold hrs_init, sis_init; wlp_simplify. econstructor; simpl in *; eauto. + split; destruct 1; econstructor; simpl in *; try rewrite H; try congruence; trivial. @@ -686,7 +686,7 @@ Proof. intros; rewrite PTree.gempty; eauto. Qed. -Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate := +Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate := DO ok_lsv <~ (if may_trap rsv lr then DO sv <~ root_happly rsv lr hrs;; @@ -730,8 +730,8 @@ Proof. + intros. exploit (ALLR a); simpl; eauto. Qed. -Lemma hrset_sreg_correct r lr rsv hrs: - WHEN hrset_sreg r lr rsv hrs ~> hrs' THEN forall ctx sis +Lemma hrs_sreg_set_correct r lr rsv hrs: + WHEN hrs_sreg_set r lr rsv hrs ~> hrs' THEN forall ctx sis (REF: ris_refines ctx hrs sis), ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis). Proof. @@ -783,6 +783,8 @@ Proof. rewrite ris_sreg_set_access. erewrite red_PTree_set_refines; intuition eauto. Qed. +Global Opaque hrs_sreg_set. +Local Hint Resolve hrs_sreg_set_correct: wlp. Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := match ib with @@ -790,10 +792,10 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := (* basic instructions *) | Bnop _ => k hrs | Bop op args dst _ => - DO next <~ hrset_sreg dst args (Rop op) hrs;; + DO next <~ hrs_sreg_set dst args (Rop op) hrs;; k next | Bload TRAP chunk addr args dst _ => - DO next <~ hrset_sreg dst args (Rload TRAP chunk addr) hrs;; + 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 _ => @@ -812,7 +814,7 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := . Definition hrexec f ib := - DO init <~ hris_init;; + DO init <~ hrs_init;; hrexec_rec f ib init (fun _ => RET Rabort). Lemma hrexec_rec_correct1 ctx ib: @@ -823,28 +825,25 @@ Lemma hrexec_rec_correct1 ctx ib: k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> - WHEN rk hrs ~> ris' THEN - rst_refines ctx ris' (k sis)) + WHEN rk hrs ~> rst THEN + rst_refines ctx rst (k sis)) hrs sis lsis sfv st (REF: ris_refines ctx hrs sis) (EXEC: sexec_rec (cf ctx) ib sis k = st) (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) (OK: si_ok ctx lsis), - WHEN hrexec_rec (cf ctx) ib hrs rk ~> hrs THEN - rst_refines ctx hrs st. + WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN + rst_refines ctx rst st. Proof. - (* induction ib; wlp_simplify. - admit. - eapply CONT; eauto. - - try_simplify_someHyps. intros OUT. + - autodestruct; try_simplify_someHyps; try congruence; intros; subst. +(* + unfold sexec_load. + exploit hrs_sreg_set_correct; eauto. eapply CONT; eauto. - intuition eauto. - econstructor; intuition eauto. - inv REF. inv H2. - intuition eauto. - - + destruct next. - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. - (* seq *) intros; subst. @@ -865,8 +864,56 @@ Proof. Qed.*) Admitted. -Definition hsexec (f: function) ib: ?? rstate := - hrexec f ib. +Lemma hrexec_correct1 ctx ib sis sfv: + get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> + (si_ok ctx sis) -> + WHEN hrexec (cf ctx) ib ~> rst THEN + rst_refines ctx rst (sexec (cf ctx) ib). +Proof. + unfold sexec; intros; wlp_simplify. + eapply hrexec_rec_correct1; eauto; simpl; try congruence; split. + - intuition eauto. + + inv H2; constructor; auto; simpl; congruence. + + inv H2; split; simpl in *; try congruence; trivial. + - intros X; simpl in *; auto. + - intros X r; inv X; simpl in *. + unfold ris_sreg_get; simpl; rewrite PTree.gempty; simpl. + reflexivity. +Qed. + +(*Lemma hrexec_rec_correct2 ctx ib: + forall rk k + (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + (CONT: forall ris sis lris rfv st, + ris_refines ctx ris sis -> + rk ris = st -> + get_routcome ctx (rk ris) = Some (rout lris rfv) -> + ris_ok ctx lris -> + rst_refines ctx (rk ris) (k sis)) + ris sis lris rfv st + (REF: ris_refines ctx ris sis) + (EXEC: rexec_rec (cf ctx) ib ris rk = st) + (SOUT: get_routcome ctx st = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). +Proof. + Admitted.*) + +Lemma hrexec_correct2 ctx ib hrs rfv: + WHEN hrexec (cf ctx) ib ~> rst THEN + get_routcome ctx rst = Some (rout hrs rfv) -> + (ris_ok ctx hrs) -> + rst_refines ctx rst (sexec (cf ctx) ib). +Proof. +Admitted. + +Lemma hrexec_simu_correct ctx ib: + WHEN hrexec (cf ctx) ib ~> rst THEN + exists st, sexec (cf ctx) ib = st /\ rst_refines ctx rst st. +Proof. + unfold hrexec; wlp_simplify. + repeat eexists. +Admitted. End CanonBuilding. @@ -1094,7 +1141,7 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := DO hC_sval <~ hCons hSVAL;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in + let hsexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) DO hst1 <~ hsexec f1 ib1;; DO hst2 <~ hsexec f2 ib2;; @@ -1104,8 +1151,15 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock): WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN symbolic_simu f1 f2 ib1 ib2. -Proof. +Proof. (* TODO *) unfold symbolic_simu; wlp_simplify. + eapply rst_simu_correct; eauto. + + intros; eapply hrexec_correct1; eauto. + 1-3: wlp_simplify. unfold hrexec. + simpl. eauto. + intuition eauto. + + intros; eapply rexec_correct2; eauto. + intros ctxz. Admitted. Global Opaque simu_check_single. Global Hint Resolve simu_check_single_correct: wlp. -- cgit