maj roadmap

1 files changed, 32 insertions, 36 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 0cbcd7d6..815aad96 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -51,7 +51,7 @@ Two possibility of branch duplications (e.g tail-duplication, loop unrolling, et
 
 Branch factorization should also be possible in BTL -> RTL pass. Example: revert "loop-unrolling".
 
-**IMPLEM NOTE:** in a first step a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes.
+**IMPLEM NOTE:** a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes.
 
 
 **CURRENT STATUS** 
@@ -64,12 +64,6 @@ Branch factorization should also be possible in BTL -> RTL pass. Example: revert
   - BTL -> RTL: TODO.
   - RTL -> BTL: started.
 
-**TODO**
-
-- lien BTL/RTL: autoriser le BTL à avoir des Bnop en plus du RTL, e.g. pour autoriser des "if-then" sans else.
-Pour faciliter le vérificateur, faire comme le Bgoto: les Bnop en "trop" ne sont autorisés que s'il y a eu une instruction RTL avant.
-Ajouter aussi un booléen (positionné par l'oracle) sur le Bnop qui indique si le "nop" existe ou pas au niveau RTL.
-
 ## Simulation modulo liveness and "Functional" semantics of BTL blocks
 
 L'approche suivie pour réaliser la simulation modulo liveness dans
@@ -83,20 +77,20 @@ On n'a pas envie de généraliser cette usine à gaz.
 
 On cherche donc une façon plus abstraite de faire... On a l'idée de
 coder la "simulation modulo liveness" dans une "simulation
-less_undef".  Ça peut rendre le cadre du test de simulation plus
+less_def".  Ça peut rendre le cadre du test de simulation plus
 simple et plus général.
 
-**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL, on pourrait
-définir une nouvelle sémantique (basée sur la même sémantique à grand
-pas dans les blocs), où c'est juste "l'entrée dans un bloc" qui change
-de sémantique. Intuitivement, cette nouvelle sémantique considèrerait
-chaque bloc comme une sorte de fonction paramétrée par les `input_regs`
-et appelée uniquement en "tailcall" (via les "goto").  C'est ce qu'on
-va appeler la "functional semantics" de BTL (l'autre étant appelée
-qqchose comme "CFG semantics" ?).
+**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL
+[BTLmatch.cfgsem], on définit une sémantique [BTL.fsem], où c'est
+juste "l'entrée dans un bloc" qui change de sémantique. Intuitivement,
+cette sémantique considère chaque bloc comme une sorte de
+fonction paramétrée par les `input_regs` et appelée uniquement en
+"tailcall" (via les "goto").  C'est ce qu'on va appeler la "functional
+semantics" de BTL (l'autre étant appelée qqchose comme "CFG semantics"
+?).
 
-Autrement dit, sur l'entrée dans un bloc pour un état (rs,m), on
-commence par mettre à Vundef tous les registres qui ne sont pas dans l'`input_regs`.
+Autrement dit, sur l'entrée dans un bloc pour un état (rs,m), on pourrait moralement
+commencer par mettre à Vundef tous les registres qui ne sont pas dans l'`input_regs`.
 
 **NOTE** cette idée de voir les blocs comme des "fonctions" correpond
 bien à la représentation "SSA" à la Appel/MLIR.  Donc cette sémantique
@@ -107,9 +101,14 @@ paramètres.
 
 **REM** pour le test d'exécution symbolique, il semble plus adapté de
 mettre les Vundef juste à la fin de la transition (précédente) plutôt
-qu'au début (de la suivante).  On pourrait aussi faire les deux (dans le détail, ça ne ferait pas exactement deux fois la même chose: 
-par exemple, quand on sort sur un call ou un builtin, le résultat du call/builtin n'est jamais dans le liveout puisqu'il va être écrasé de toute façon pendant la transition, 
-mais il peut être -- ou pas -- dans le livein de la transition suivante dans ce même bloc).
+qu'au début (de la suivante): c'est d'ailleurs plus proche de la vision SSA.  
+
+En fait, on pourrait faire les deux (dans le détail, ça ne ferait pas
+exactement deux fois la même chose: par exemple, quand on sort sur un
+call ou un builtin, le résultat du call/builtin n'est jamais dans le
+liveout puisqu'il va être écrasé de toute façon pendant la transition,
+mais il peut être -- ou pas -- dans le livein de la transition
+suivante dans ce même bloc).
 
 Avoir une initialisation à Vundef en début de bloc permettrait de
 faire une analyse des expressions mal initialisées - par exemple à
@@ -117,24 +116,20 @@ 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).
 
-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.
+Donc, dans un premier temps, la BTL.fsem 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. 
+1. See [BTL.fsem]
+2. fsem -> cfgsem: fait (ou presque).
+3. cfgsem -> fsem: a faire (via verif de liveness).
 
 ## "Basic" symbolic execution / symbolic simulation
 
-We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. 
+We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.fsem. 
 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é.
 
 **STATUS**
@@ -353,15 +348,16 @@ Extends the symbolic simulation test to support invariants at block entry, inclu
 
 **IDEAS**
 
-- En pratique, il faudra peut-être affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie.
+- En pratique, il faudrait affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie.
+Une solution possible: calquer Bjumptable sur Bcond (c-a-d autoriser les Bjumptable en milieu de blocs). On pourrait étendre la prédiction de branchement par profiling aux jumptables (par exemple, avoir des superblocks avec des jumptables au milieu). Un autre intérêt: simplifier le support pour des formes SSA partielles (cf. ci-dessous).
 
 - Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins).
 
 ## Support of SSA-optimizations
 
-Extends BTL with "register renamings" at exits.
+Minimum feature: extends BTL with "register renamings" at exits. This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.
 
-This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.
+Maximum feature: add a basic instruction that performs parallel renaming of registers. If we also support Bjumptable in the middle of a block (see above), this simple feature would suffice to represent a very general notion of "partial SSA forms": since they could appear in the middle of a block, or just before an exit (such a parallel assignment would be forbidden in BTL<->RTL matching).
 
 ## Alias analysis in the symbolic simulation