avancement roadmap

1 files changed, 28 insertions, 11 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 32d0b365..6042803d 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -3,8 +3,8 @@
 BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation).
 It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event.
 The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules.
-The only info required from oracles: a "dupmap" mapping block entries.
-In contrast, the "global" optimizations would require some invariants annotations at block entry (provided by oracles).
+The main info required from oracles: a "dupmap" mapping block entries (and maybe strategies for controlling path explosion during symbolic execution -- see below).
+Moreover, the "global" optimizations would require some invariants annotations at block entry (provided by oracles).
 
 Examples of optimizations that we aim to support:
 
@@ -16,6 +16,9 @@ Examples of optimizations that we aim to support:
 
 We sketch below the various kinds of supported optimizations in development order...
 
+Remark that we may port most of the current optimizations from RTL to BTL (even maybe, register allocation).
+However, RTL will probably remain useful for "fine-tuned" duplication that crosses block boundaries (e.g. Duplicate module).
+
 ## Introduction
 
 En gros la syntaxe d'un bloc BTL est définie par:
@@ -83,7 +86,7 @@ coder la "simulation modulo liveness" dans une "simulation
 less_undef".  Ça peut rendre le cadre du test de simulation plus
 simple et plus général.
 
-**Idée** à côté de la sémantique "à la RTL" pour BTL, on pourrait
+**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
@@ -102,11 +105,21 @@ 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 (précédente) plutôt qu'au début (de la suivante).
+**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).
+
+Avoir une initialisation à Vundef en début de bloc permettrait de
+faire une analyse des expressions mal initialisées - par exemple à
+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.
+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.
@@ -119,11 +132,13 @@ En fait, pour le test d'exécution symbolique, il semble plus simple de mettre l
 
 ## "Basic" symbolic execution / symbolic simulation
 
-We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics.
+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).
 
 **CURRENT STATUS**
 
@@ -334,9 +349,13 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina
 
 ## Invariants at block entry
 
-Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers.
+Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
+
+**IDEAS**
 
-Case-study: support of strength-reduction.
+- 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.
+
+- 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
 
@@ -346,6 +365,4 @@ This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.
 
 ## Alias analysis in the symbolic simulation
 
-A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf)
-
-
+A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf)