From 3348c88e1d61d109a8c0388ec421ac6bf17a5c6b Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 4 Jun 2021 09:07:45 +0200 Subject: progress in BTL_SEsimuref --- scheduling/BTL_SEsimuref.v | 56 ++++++++++++++++++++++++++++++++++++---------- scheduling/BTL_SEtheory.v | 34 +++++++++------------------- scheduling/BTL_Scheduler.v | 22 ++++++++++++++++++ 3 files changed, 77 insertions(+), 35 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index c322a9a5..a4da4291 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -191,14 +191,14 @@ Inductive rstate := . Inductive rst_simu: rstate -> rstate -> Prop := - | Rfinal_simu ris1 ris2 rfv1 rfv2: - ris_simu ris1 ris2 -> - rfv_simu rfv1 rfv2 -> - rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2) - | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2: - rst_simu rifso1 rifso2 -> - rst_simu rifnot1 rifnot2 -> - rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2) + | Rfinal_simu ris1 ris2 rfv1 rfv2 + (RIS: ris_simu ris1 ris2) + (RFV: rfv_simu rfv1 rfv2) + : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2) + | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2 + (IFSO: rst_simu rifso1 rifso2) + (IFNOT: rst_simu rifnot1 rifnot2) + : rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2) | Rabort_simu: rst_simu Rabort Rabort (* TODO: extension à voir dans un second temps ! | Rcond_skip cond rargs rifso1 rifnot1 rst: @@ -225,6 +225,8 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop := : rst_refines ctx Rabort Sabort . +Local Hint Resolve ris_simu_correct rvf_simu_correct: core. + Lemma rst_simu_correct rst1 rst2: rst_simu rst1 rst2 -> forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*), @@ -233,7 +235,37 @@ Lemma rst_simu_correct rst1 rst2: (* ok1 -> ok2 -> *) sstate_simu ctx st1 st2. Proof. - induction 1; simpl; auto. - - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. - inv REF1. inv REF2. inv SEM1. -Admitted. \ No newline at end of file + induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1; + inv REF1; inv REF2; simpl in *; inv SEM1; auto. + - (* final_simu *) + do 2 eexists; intuition; eauto. + exploit sem_sok; eauto. + erewrite OK_EQUIV; eauto. + intros ROK1. + exploit ris_simu_ok_preserv; eauto. + - (* cond_simu *) + destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence. + generalize RCOND0. + erewrite <- seval_condition_preserved, RCOND by eauto. + intros SCOND0; rewrite <- SCOND0 in RCOND0. + erewrite <- SCOND0. + destruct b; simpl. + * exploit IHrst_simu1; eauto. + * exploit IHrst_simu2; eauto. +Qed. + + +(** TODO: could be useful ? +Lemma seval_condition_valid_preserv ctx cond args sm b + (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) + :seval_condition ctx cond args sm = Some b -> + seval_condition ctx cond args Sinit = Some b. +Proof. + unfold seval_condition; autodestruct; simpl; try congruence. + intros EVAL_LIST. + autodestruct; try congruence. + intros MEM COND. rewrite <- COND. + eapply cond_valid_pointer_eq; intros. + exploit VALID_PRESERV; eauto. +Qed. +*) \ No newline at end of file diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 557541ce..9ab64d7d 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1064,32 +1064,10 @@ Qed. (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) -(* -Definition equiv_input_regs (f1 f2: BTL.function): Prop := - (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) - /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). - -Lemma equiv_input_regs_union f1 f2: - equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. -Proof. - intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. - generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. - do 2 autodestruct; intuition; try_simplify_someHyps. - intros; exploit EQS; eauto; clear EQS. congruence. -Qed. - -Lemma equiv_input_regs_pre f1 f2 tbl or: - equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. -Proof. - intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. -Qed. -*) - Record simu_proof_context {f1 f2: BTL.function} := Sctx { sge1: BTL.genv; sge2: BTL.genv; sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; - (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *) ssp: val; srs0: regset; sm0: mem @@ -1156,7 +1134,7 @@ Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sistate_simu ctx sis1 sis2 - /\ sfv_simu ctx sfv1 sfv2 + /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) . Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). @@ -1261,6 +1239,16 @@ Proof. rewrite smem_eval_preserved; auto. Qed. +(* TODO: useless ? +Lemma run_sem_isstate_preserved sis: + run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis. +Proof. + induction sis; simpl; eauto. + erewrite seval_condition_preserved. + repeat (autodestruct; auto). +Qed. +*) + (* additional preservation properties under this additional hypothesis *) Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index bcddcf5d..ec83b3c1 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -9,6 +9,28 @@ Axiom scheduler: BTL.function -> BTL.code. Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". +(* TODO: could be useful ? +Definition equiv_input_regs (f1 f2: BTL.function): Prop := + (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) + /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). + +Lemma equiv_input_regs_union f1 f2: + equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. +Proof. + intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. + generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. + do 2 autodestruct; intuition; try_simplify_someHyps. + intros; exploit EQS; eauto; clear EQS. congruence. +Qed. + +Lemma equiv_input_regs_pre f1 f2 tbl or: + equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. +Proof. + intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. +Qed. +*) + + (* a specification of the verification to do on each function *) Record match_function (f1 f2: BTL.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; -- cgit