From abfc8509ec4686924095c1328179fa06766dc496 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 2 Jun 2021 08:20:58 +0200 Subject: the current "high-level" specification of the simulation test will not work ! --- scheduling/BTL_SEtheory.v | 58 +++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 48 insertions(+), 10 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index c7a44153..72789121 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1022,38 +1022,76 @@ Qed. (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) -Record simu_proof_context := Sctx { +(* +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; sstk1: list BTL.stackframe; sstk2: list BTL.stackframe; sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; + (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *) ssp: val; srs0: regset; sm0: mem }. +Arguments simu_proof_context: clear implicits. -Definition bctx1 f1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition bctx2 f2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition sstate_simu f1 f2 (ctx: simu_proof_context) (st1 st2: sstate) := - forall t s1, sem_sstate (bctx1 f1 ctx) t s1 st1 -> - exists s2, sem_sstate (bctx2 f2 ctx) t s2 st2 /\ equiv_state s1 s2. -Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2). +(* TODO: A REVOIR. L'approche suivie ne marche pas !!! + +le [equiv_state] ci-dessous n'est pas assez général + => il faut un [match_state] qui va dépendre de [BTL_Scheduler.match_function] (dans le [match_stackframe]). + +Or, le [sstate_simu] qu'on cherche à définir ici, c'était pour définir ce [match_function]: circularité ! + +Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ? + +Pas sûr que ça marche, on aura aussi la dépendance circulaire entre [simu_proof_context] et [match_function] ! + +Autre solution: définir [sfval_simu] syntaxiquement comme dans [RTLpath_SEtheory] pour éviter le problème de circularité ! + +*) +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2: sstate) := + forall t s1, sem_sstate (bctx1 ctx) t s1 st1 -> + exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2. + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). Theorem symbolic_simu_correct f1 f2 ib1 ib2: symbolic_simu f1 f2 ib1 ib2 -> - forall ctx t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + forall (ctx: simu_proof_context f1 f2) t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. Proof. unfold symbolic_simu, sstate_simu. intros SIMU ctx t s1 STEP1. - exploit (sexec_correct (bctx1 f1 ctx)); simpl; eauto. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. intros; exploit SIMU; eauto. intros (s2 & SEM1 & EQ1). - exploit (sexec_exact (bctx2 f2 ctx)); simpl; eauto. + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. -- cgit