diff options
-rw-r--r-- | scheduling/BTL_SEtheory.v | 24 | ||||
-rw-r--r-- | scheduling/BTL_Scheduler.v | 32 | ||||
-rw-r--r-- | scheduling/BTL_Schedulerproof.v | 2 |
3 files changed, 22 insertions, 36 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index ea7082a9..3083ca71 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1020,10 +1020,7 @@ Proof. inversion SEXEC. Qed. -(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] - -TODO: à revoir complètement. Il faut passer le dupmap en paramètre et match les états symboliques modulo le dupmap. -*) +(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) Record simu_proof_context := Sctx { sge1: BTL.genv; @@ -1031,7 +1028,7 @@ Record simu_proof_context := Sctx { 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; (* REM: equiv_stackframe n'est pas suffisant, il faut le dupmap dedans ! *) + sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; ssp: val; srs0: regset; sm0: mem @@ -1040,24 +1037,23 @@ Record simu_proof_context := Sctx { 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). -(* TODO: A REVOIR ! *) 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 ctx ib1 ib2: sstate_simu f1 f2 ctx (sexec (f1 ctx) ib1) (sexec (f2 ctx) ib2). +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2). -Theorem symbolic_simu_correct f1 f2 ctx ib1 ib2: - symbolic_simu ctx ib1 ib2 -> - forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> - exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. +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 -> + 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 t s1 STEP1. - exploit (sexec_correct (bctx1 ctx)); simpl; eauto. + intros SIMU ctx t s1 STEP1. + exploit (sexec_correct (bctx1 f1 ctx)); simpl; eauto. intros; exploit SIMU; eauto. intros (s2 & SEM1 & EQ1). - exploit (sexec_exact (bctx2 ctx)); simpl; eauto. + exploit (sexec_exact (bctx2 f2 ctx)); simpl; eauto. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 8cf9635c..faeb58cd 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -5,36 +5,24 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking BTL_SEtheory. (** External oracle *) -Axiom scheduler: BTL.function -> BTL.code * node * (PTree.t node). +Axiom scheduler: BTL.function -> BTL.code. -(* FAKE: A REVOIR avec BTL_SEtheory... *) -Definition symbolic_simu (dupmap: PTree.t node) (f1 f2: BTL.function) (pc1 pc2: node): Prop := True. - -Record match_function (dupmap: PTree.t node) (f1 f2: BTL.function): Prop := { +(* 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; preserv_fnparams: fn_params f1 = fn_params f2; preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; - preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint); - dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> symbolic_simu dupmap f1 f2 pc1 pc2; + preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; + symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); }. -Definition verified_scheduler (f: BTL.function) := - let (tcte, dupmap) := scheduler f in - let (tc, te) := tcte in - let f' := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in - OK (f', dupmap). (* TODO: fixme *) - -Program Definition transf_function (f: BTL.function): - { r : res BTL.function | forall f', r = OK f' -> exists dm, match_function dm f f'} := - match (verified_scheduler f) with - | Error e => Error e - | OK (tf, dm) => OK tf - end. -Next Obligation. -Admitted. +Definition transf_function (f: BTL.function) := + (* TODO: fixme *) + OK (BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f)). Definition transf_fundef (f: fundef) : res fundef := - transf_partial_fundef (fun f => proj1_sig (transf_function f)) f. + transf_partial_fundef (fun f => transf_function f) f. Definition transf_program (p: program) : res program := transform_partial_program transf_fundef p. diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 049dc6b1..c8c2a76f 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -24,6 +24,8 @@ Let tpge := Genv.globalenv tprog. Theorem transf_program_correct: forward_simulation (fsem prog) (fsem tprog). +Proof. + eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *) Admitted. End PRESERVATION. |