IDEE pour la STRENGTH-REDUCTION

1 files changed, 43 insertions, 1 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 954143c1..bfbc1e03 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -346,13 +346,55 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina
 
 Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
 
-**IDEAS**
+**PRELIMINARY IDEAS**
 
 - 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 ?
 
 - 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).
 
+**EXAMPLE OF STRENGTH REDUCTION**
+
+On veut passer du code C1:
+
+    init: // inputs: int *t,  int n, int s 
+    int i=0;
+    loop: // inputs: int *t,  int n, int s, int i 
+        if (i >= n) goto exit;
+        s += t[i];
+        i += 1;
+        goto loop;
+    exit: // inputs: int *t,  int s
+    
+au code C2:
+
+    init: // inputs: int *t,  int n, int s 
+    int *ti = t;
+    int *tn = t+n;
+    loop: // inputs: int *t,  int s, int *ti, int *tn
+        if (ti >= tn) goto exit;
+        s += *ti;
+        ti += 4;
+        goto loop;
+    exit; // inputs: int *t,  int s
+        
+Pour donner la correspondance entre les variables des 2 blocs, pour chaque entrée "pc", on introduit une "fonction" de C1@pc.(inputs) -> C2@pc.(inputs).
+
+Typiquement, cette fonction est codable comme un map associant une valeur symbolique sur les C1@pc.(inputs) aux variables de C2@pc.(inputs). Exemple:
+
+    init: // map vide (identité)
+    loop:
+        ti = t+i
+        tn = t+n
+    exit: // map vide (identité)
+ 
+Si on note `TRANSFER` cette fonction, alors la vérification par
+exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo
+`TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec
+`TRANSFER(pc); ib2` pour la simulation symbolique usuelle.
+ 
+ Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`.
+
 ## 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.