end of BTL_SEtheory w.r.t fsem

1 files changed, 18 insertions, 18 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 6042803d..0cbcd7d6 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -117,37 +117,37 @@ partir du bloc d'entrée de la fonction. Ça semble complémentaire de
 l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une
 combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite).
 
-**IMPLEM PLAN**
-
-1. définir the "functional semantics" of BTL (dans un premier temps, avec uniquement Vundef en sortie de bloc). Rem: en pratique, la "functional semantics" est définie pour être une "concrétisation" de la sémantique symbolique. Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée.
-2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep").
-3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics.
-   en gros: on implémente un vérificateur des infos de liveness.
-   c'est la correction du "input_regs" qui garantit que la simulation est correct.
-   La preuve devrait normalement être très similaire à RTLpathLivegenproof. 
+Donc, dans un premier temps, la "functional semantics" encode/abstrait la notion de "liveout" pour le test d'exécution symbolique. 
+Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée.
 
 **STATUS**
 
 1. See [BTL.fsem]  (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem)
 
+**TODO**
+
+1. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep").
+2. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics.
+   en gros: on implémente un vérificateur des infos de liveness.
+   c'est la correction du "input_regs" qui garantit que la simulation est correct.
+   La preuve devrait normalement être très similaire à RTLpathLivegenproof. 
+
 ## "Basic" symbolic execution / symbolic simulation
 
 We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. 
 Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté.
 
-**IMPLEM NOTE**
-
-- use Continuation Passing Style for an easy recursive generation of "all execution paths".
-- dans l'etat concret, prévoir un booleen qui indique la valeur symbolique par defaut des registres: deux cas, soit "Input" (valeur initiale du registre), soit "Sundef" (valeur Vundef).
+**STATUS**
 
-**CURRENT STATUS**
+- BTL_SEtheory: DONE
+ - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem
+ - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem).
 
-- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.semantics
+**TODO**
 
-**next steps**
-- preservation proof w.r.t  BTL.fsem.
-- high-level specification of "symbolic simulation"
-- ...
+1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof).
+2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ?
+Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ?
 
 ## Port of RTLpath optimizations to BTL