diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 15:56:44 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 15:56:44 +0200 |
commit | 5b67f8284c3a98581f4da9b065a738fc534480c4 (patch) | |
tree | c3c299be4a66c19045a81e212e48505c243400d0 /scheduling/BTL_SEtheory.v | |
parent | b79d0a04787d9234cf580841bf58e592fe4ab3ee (diff) | |
download | compcert-kvx-5b67f8284c3a98581f4da9b065a738fc534480c4.tar.gz compcert-kvx-5b67f8284c3a98581f4da9b065a738fc534480c4.zip |
archi pour la verif du scheduler
Diffstat (limited to 'scheduling/BTL_SEtheory.v')
-rw-r--r-- | scheduling/BTL_SEtheory.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 5b15fe9b..ea7082a9 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1020,7 +1020,10 @@ Proof. inversion SEXEC. Qed. -(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) +(** * 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. +*) Record simu_proof_context := Sctx { sge1: BTL.genv; @@ -1028,24 +1031,23 @@ 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; - sf1: BTL.function; - sf2: BTL.function; + sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; (* REM: equiv_stackframe n'est pas suffisant, il faut le dupmap dedans ! *) ssp: val; srs0: regset; sm0: mem }. -Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0). +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 sstate_simu (ctx: simu_proof_context) (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. +(* 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 ctx ib1 ib2: Prop := sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2). +Definition symbolic_simu f1 f2 ctx ib1 ib2: sstate_simu f1 f2 ctx (sexec (f1 ctx) ib1) (sexec (f2 ctx) ib2). -Theorem symbolic_simu_correct ctx ib1 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. |