correction de l'idee de la Functional semantics

1 files changed, 17 insertions, 26 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index bd70e273..39ea12d0 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -73,40 +73,36 @@ 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.
+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. le traitement de `pre_output_regs` dans RTLpathScheduler, etc).
+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
+**Idée** à 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ère
+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" ?).
 
 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).
+commence 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
+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.
 
-**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.
+En fait, pour le test d'exécution symbolique, il semble plus simple de mettre les Vundef à la fin de la transition...
 
 **IMPLEM PLAN**
 
@@ -125,16 +121,11 @@ We will implement a "basic" (e.g without rewriting rules) "less_undef" simulatio
 **IMPLEM NOTE**
 
 - 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 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).
+- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t  BTL.FunctionalSemantics.
 
 ## Port of RTLpath optimizations to BTL