diff options
-rw-r--r-- | scheduling/BTLroadmap.md | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 39ea12d0..32d0b365 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -102,7 +102,7 @@ totales) dans BTL. Pour l'encodage de SSA, il suffira d'étendre le mécanisme d'initialisation du "rs0" d'un bloc avec un passage de paramètres. -En fait, pour le test d'exécution symbolique, il semble plus simple de mettre les Vundef à la fin de la transition... +En fait, pour le test d'exécution symbolique, il semble plus simple de mettre les Vundef à la fin de la transition (précédente) plutôt qu'au début (de la suivante). **IMPLEM PLAN** @@ -113,6 +113,9 @@ En fait, pour le test d'exécution symbolique, il semble plus simple de mettre l c'est la correction du "input_regs" qui garantit que la simulation est correct. La preuve devrait normalement être très similaire à RTLpathLivegenproof. +**STATUS** + +1. See [BTL.fsem] (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem) ## "Basic" symbolic execution / symbolic simulation @@ -124,8 +127,12 @@ We will implement a "basic" (e.g without rewriting rules) "less_undef" simulatio **CURRENT STATUS** -- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms. -- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t BTL.FunctionalSemantics. +- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.semantics + +**next steps** +- preservation proof w.r.t BTL.fsem. +- high-level specification of "symbolic simulation" +- ... ## Port of RTLpath optimizations to BTL |