fix roadmap on "Simulation modulo liveness"

1 files changed, 61 insertions, 24 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 2f630a72..dde2090c 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -63,37 +63,74 @@ Branch factorization should also be possible in BTL -> RTL pass. Example: revert
 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
+RTLpath est compliquée à adapter sur BTL.  En effet, un état
+symbolique RTLpath correspond à un état symbolique BTL très
+particulier: toutes les "feuilles" (les `Sfinal`) sont des `Sgoto`
+sauf éventuellement une.  Or, dans RTLpath, le traitement de l'info de liveness sur
+cette feuille particulière est très adhoc et laborieux (cf. `pre_output_regs`).  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
+simple et plus général.
+
+L'idée de départ: "Extends BTL with the possibility of destroying a
+set of registers at each exit (a destroyed register is simply set to
+Vundef)" en prouvant une simulation "less_undef" n'est pas assez
+générale!  Ça n'autorise pas à introduire de "nouveaux" registres dans
+le bloc transformé, juste à donner n'importe quelle valeur aux
+registres "hors-liveout".
+
+**Idée corrigée** à côté de la sémantique "à la RTL" pour BTL, on
+définit 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è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
+remplace juste cet état par un nouvel état (rs0,m) où dans rs0, tous les registres
+sont initialisés à Vundef sauf ceux du `input_regs` qui sont
+initialisés comme une copie de "rs". In fine, on applique le
+"iblock_step" sur cet état (rs0,m).
+
+**NOTE** cette idée de voir les blocs comme des "fonctions" correpond bien à la représentation "SSA" à la Appel/MLIR. 
+Donc cette sémantique peut servir de base pour un support de formes SSA (partielles ou 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.
+
+**IMPLEM PLAN**
+
+1. définir the "functional semantics" of BTL.
+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. 
+
 
 ## "Basic" symbolic execution / symbolic simulation
 
-IMPLEM PLAN in two steps:
+We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics.
 
-1. a very basic version without rewriting rules, and without support for simulation modulo-liveness.
+**IMPLEM NOTE**
 
-2. Support a "SVundef" symbolic value, and implement symbolic simulation wrt "less_undef" relation. 
-This will allow more general rewriting rules and will generalize modulo-liveness (see next section).
+- use Continuation Passing Style for an easy recursive generation of "all execution paths".
+- pour implementer la "functional semantics", il faut changer
+  légèrement la sémantique du map qui associe une valeur symbolique à
+  chaque registre. En RTLpath, un registre "absent" de la map était considéré comme positionné à sa valeur initial.
+  Là, il faudra considérer qu'il vaut Vundef (il y a une valeur symbolique spéciale à ajouter !)
 
 **CURRENT STATUS**
 
-- model of symbolic execution in Continuation-Passing Style, with basic "correctness" thm ("completness" not yet done).
-
-## Simulation modulo liveness
-
-Extends BTL with the possibility of destroying a set of registers at each exit (a destroyed register is simply set to Vundef).
-
-We can the provide a "MarkUnused" pass of BTL -> BTL that insert these destructions at each exit using liveness info !
-(NB: the liveness info could be provided by the RTL -> BTL oracle like on RTLpath).
-
-In the symbolic execution, destroying a register corresponds to associate it SVundef value.
-
-NB: this approach through "destroyed registers" and "SVundef" seems more modular (thus simpler) and more general than the current approach on RTLpath.
-
-The proof of "simulation modulo liveness" of a BTL B1 by a BTL B2 will simply corresponds to compose two forward simulations:  B1 --> MarkUnused(B1) --> B2.
-
-**IMPLEM NOTE:** "MarkUnused" checks the correctness of liveness informations while performing its transformation.
-It should computes alive register from block entry, by forward proceeding of "internal instructions" (like in RTLPathLivegen).
-When arriving on a final instruction, we marked as "destroyed" all alive registers that are not in the input registers of the exit
-Semantically, the destruction of registers happens "in parallel" of the final step of the block.
+- 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 
+(dans une première étape, on peut laisser le "less_undef" de côté: ce sera facile à ajouter quand le cadre sera en place).
 
 ## Port of RTLpath optimizations to BTL
 
@@ -301,7 +338,7 @@ Case-study: support of strength-reduction.
 
 ## Support of SSA-optimizations
 
-Extends BTL with "register renamings" at exits (in a sense, "register renaming" extends the feature of "register destroying").
+Extends BTL with "register renamings" at exits.
 
 This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.