BTLroadmap: combinaison liveness et invariants ?

1 files changed, 47 insertions, 9 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 3d799235..1514c5d4 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -350,18 +350,39 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina
 
 **Rem** les mécanismes de propagation/réécritures décrits ci-dessus peuvent être aussi très utile pour la simulation symbolique modulo invariants (cf. ci-dessous) !
 
-## Invariants at block entry
+## Peut-on coder l'égalité modulo liveness comme un cas simple d'invariant symbolique (et faire la vérif de liveneness par execution symbolique) ?
 
-Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
+On peut peut-être simplifier le cadre actuel pour rendre l'intégration des invariants symboliques plus facile !! Une piste à creuser...
+
+Si la sémantique `BTL.fsem` a permis de rendre l'architecture un peu plus modulaire (mais sans vraiment simplifier sur le fond). 
+Elle ne simplifie pas vraiment l'intégration de la liveness avec les invariants.
+Une approche qui pourrait réellement simplifier: voir le raisonnement modulo liveness comme un cas particulier d'invariant symbolique. 
+
+**Idée** pour tout chemin d'exécution passant de `pc` et `pc'`, on ramène la simulation modulo liveness de `ib1` par `ib2` au test:
+    
+    [ib1;str_inputs(pc')] lessdef [str_inputs(pc);ib2]
+    
+**Avantages possibles**
 
-**PRELIMINARY IDEAS**
+- plus de verif de liveness spécifique.
+- plus de sémantique `BTL.fsem`
+- les `str_inputs` ne seraient plus dans l'exécution symbolique, mais dans le test de simulation: ça évite les difficultés sur les jumptables.
 
-- 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 (un peu) le support pour des formes SSA partielles (cf. ci-dessous). Ceci dit, ça compliquerait les choses à plein d'endroits (type Coq [iblock] mutuellement inductif avec [list_iblock] pour avoir les bons principes d'inductions, etc) pour des gains minimes en pratiques ?
+Par contre, il faut réintroduire une preuve `lessdef` modulo liveness dans `BTL_Schedulerproof`.
 
-- 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).
+### Plan d'implem. incrémentale (dans une branche)
+
+1. Repartir d'une version de BTL sans info de liveness pour simplifier au maximum!! (ie on supprime la semantique fsem et on repart sur cfgsem).
+2. Introduire la preuve `lessdef` modulo liveness dans `BTL_Schedulerproof` en *supposant* qu'on a le test de simulation symbolique qui nous arrange. 
+   L'idée est de dégager des conditions suffisantes sur le test de simulation symbolique.
+3. Réaliser le test de simulation symbolique.
+
+## Symbolic Invariants at block entry
+
+Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
 
-**EXAMPLE OF STRENGTH REDUCTION**
+
+### EXAMPLE OF STRENGTH REDUCTION
 
 On veut passer du code C1:
 
@@ -382,7 +403,7 @@ au code C2:
     loop: // inputs: int *t,  int s, int *ti, int *tn
         if (ti >= tn) goto exit;
         s += *ti;
-        ti += 4;
+        ti += 1; // i.e. sizeof(int)
         goto loop;
     exit; // inputs: int *t,  int s
         
@@ -405,11 +426,28 @@ Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des
 
 **REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`...
 
+### Comment gérer le cas des registres résultat de call et builtin ?
+
+Rem: c'est la gestion de ces cas particuliers qui conduit à la notion de `pre_output_regs` (ou `BTL.pre_input`) dans la verif de la simulation modulo liveness.
+On va retrouver ça dans la verif de la simulation modulo invariants symboliques.
+Mais pas évident à éviter. 
+
+Concrètement, on ne pourra pas mettre d'invariant qui porte sur le résultat d'un call ou d'un builtin (à part un pur renommage de registre).
+
+### GENERALISATION (What comes next ?)
+
+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).
+
+En gros, on pourrait passer d'invariants purement symboliques à des invariants combinant valeurs symboliques et valeurs abstraites.
+
 ## Support of SSA-optimizations
 
 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.
 
-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).
+Maximum feature: add also a basic instruction that performs parallel renaming of registers. 
+This simple feature would help to represent a very general notion of "partial SSA forms": since they could appear in the middle of a block.
+
+In both case, such register renamings would be forbidden in BTL<->RTL matching (SSA-optimizations could only happen within BTL passes).
 
 ## Alias analysis in the symbolic simulation