précision du roadmap

1 files changed, 230 insertions, 4 deletions

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 27e74de5..05dcb95e 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -16,6 +16,29 @@ Examples of optimizations that we aim to support:
 
 We sketch below the various kinds of supported optimizations in development order...
 
+## Introduction
+
+En gros la syntaxe d'un bloc BTL est définie par:
+
+    Inductive iblock: Type :=
+    | ... (* instructions basiques ou "finales" (call, return, goto, etc) *)
+    | Bseq (b1 b2: iblock)  (* séquence de deux blocs *)
+    | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock)  (* if-then-else *)
+
+Le modèle de base de l'exécution symbolique représente un tel bloc par un état symbolique de type:
+
+    Inductive sstate :=
+    | Sfinal (sis: sistate) (sfv: sfval)
+    | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate)
+    | Sabort
+    .
+
+où `sistate` est un PPA (preconditioned parallel assignment) des registres et `sfval` représente un branchement (call, return, goto, etc).
+    
+Autrement dit, un état symbolique représente tous les chemins
+d'exécution possibles par une sorte de gros BDD ayant sur les feuilles
+un `Sfinal` (ou un `Sabort` s'il manque une instruction de branchement sur ce chemin).
+
 ## Block boundaries, branch duplication or factorization
 
 Two possibility of branch duplications (e.g tail-duplication, loop unrolling, etc):
@@ -25,12 +48,21 @@ Two possibility of branch duplications (e.g tail-duplication, loop unrolling, et
 
 Branch factorization should also be possible in BTL -> RTL pass. Example: revert "loop-unrolling".
 
-**IMPLEM NOTE:** a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes.
+**IMPLEM NOTE:** in a first step a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes.
+
 
 **CURRENT STATUS** 
 
-- verifier: specified but not yet implemented.
-- BTL -> RTL: proof started.
+- verifier: implemented and proved w.r.t match_iblock specification.
+- BTL -> RTL: done.
+- RTL -> BTL: started.
+
+**TODO**
+
+- lien BTL/RTL: autoriser le BTL à avoir des Bnop en plus du RTL, e.g. pour autoriser des "if-then" sans else.
+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.
+
 
 ## "Basic" symbolic execution / symbolic simulation
 
@@ -41,7 +73,9 @@ IMPLEM PLAN in two steps:
 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).
 
-**IMPLEM NOTE:** use a symbolic execution in Continuation-Passing Style, in order to have of simple handling of "side-exits" within "branch unfolding". 
+**CURRENT STATUS**
+
+- model of symbolic execution in Continuation-Passing Style, with basic "correctness" thm ("completness" not yet done).
 
 ## Simulation modulo liveness
 
@@ -67,6 +101,198 @@ Semantically, the destruction of registers happens "in parallel" of the final st
 - Port rewriting rules of RTLpath.
 - Justus's "poor man SSA" + if-lifting.
 
+## Efficient comparison (guided by oracles) of "if-then-else" sequences.
+
+Le pb est complexe. Comparer des expressions booleennes contenant juste des variables booleennes est déjà NP-complet, avec "explosion exponentielle" dans le pire cas.
+
+Approche proposée: utiliser un mécanisme de vérification "simple", basée sur une comparaison par execution symbolique de "tous" les chemins d'execution (cf Intro ci-dessus).
+Ça pète exponentiellement dans le pire cas: mais on pourra contrôler ce risque d'explosion par les oracles...
+
+Ci-dessous, on liste quelques "techniques" de collaboration oracle/vérificateur pour contrôler l'explosion des chemins.
+Idée: les conditions comportent une liste d'annotations qui permet le guidage du vérificateur par l'oracle.
+
+### Contrôle des "joins internes" dans le bloc. 
+
+Si dans le bloc, toute condition a au plus un "predecesseur" (au sens
+du CFG RTL) dans le bloc: alors le nombre de "chemins sémantiques"
+(explorés par l'exécution symbolique) est identique au nombre de
+"branches syntaxiques" (présents dans le code). Une façon simple de
+contrôler l'explosion de l'exécution symbolique est de fabriquer (avec
+les oracles) des blocs avec un nombre borné (petit) de "joins
+internes".
+
+**Exemple d'application: généralisation des superblocks**
+
+On considère le bloc BTL ci-dessous (où les `i*` sont des séquences d'instructions basiques sans branchement):
+   
+    i0;
+    if (c1) { i1 } else { i1'; goto pc1 }
+    if (c2) { i2; goto pc2 } else { i2' }
+    if (c3} { i3; goto pc3 } else { i3'; goto pc3' }
+
+Sur un tel bloc, il n'y a aucun "join interne" (l'exécution symbolique est donc linéaire).
+Mais représenter en RTLpath un tel bloc nécessite au moins 4 blocks (1 superbloc et 3 basic-blocs):
+
+    i0; c1; i1; c2; i2'; i3'; goto pc3'
+    i1'; goto pc1 
+    i2; goto pc2
+    i3; goto pc3
+
+La vérification BTL sur le gros bloc ne prendra à priori pas plus de
+temps que la vérification RTLpath cumulée des 4 "petits" blocs. Mais
+la vérification BTL sera plus *puissante*, puisque que quand on va
+vérifier les chemins d'exécutions correspondant à ceux des 3
+basic-blocs, on aura le `i0` en plus dans l'état symbolique (i.e. un
+"contexte d'exécution" plus précis).
+
+**Autre exemple d'application: le if-lifting à la Justus**
+
+Le superblock suivant:
+    
+    y1 = e1(x)
+    x = e2(a)
+    y2 = e3(x)
+    if (c[x]) { goto pc  } else { i4; goto pc' }
+     
+peut être directement montré équivalent à
+
+    x' = e2(a)   // x' un registre "frais" (pas dans les "liveout")
+    if (c[x']) { 
+        y1 = e1(x);
+        x = x';
+        y2 = e3(x);
+        goto pc
+    } else {
+        y1 = e1(x);
+        x = x';
+        y2 = e3(x);
+        i4; 
+        goto pc'
+    }
+   
+Ici, la duplication de branche a donc lieu en BTL.
+
+L'exécution symbolique de ces deux blocs va produire deux BDD comparables (avec comparaison des feuilles modulo liveness).
+
+### Comparaison des BDD (modulo réordonnancement des conditions ?)
+
+On peut avoir envie de montrer que les deux blocs ci-dessous sont équivalents (si les dépendences sur les variables le permettent):
+
+    if (c1) { i1 } else { i1' }
+    if (c2) { i2 } else { i2' }
+    
+et
+
+    if (c2) { i2 } else { i2' }
+    if (c1) { i1 } else { i1' }
+
+Ça revient (en gros) à comparer les BDD:
+   
+    if (c1) { if (c2) {i1;i2} else {i1;i2'} } else { if (c2) {i1';i2} else {i1';i2'} }
+
+et 
+
+    if (c2) { if (c1) {i2;i1} else {i2;i1'} } else { if (c1) {i2';i1} else {i2';i1'} }
+
+Pour gérer ça, on peut faire des "Ordered BDD": l'oracle du **bloc
+transformé** annote (certaines) conditions avec des numéros de façon à
+ce l'exécution symbolique du bloc transformé produise un "BDD" qui
+correspond à celui du bloc d'origine (cf. "Principe"
+ci-dessous). Cependant, il semble difficile d'appliquer complètement
+les techniques de mémoïsation des BDD ayant des booléens sur les
+feuilles.  Car ici on veut effectuer une comparaison sur des feuilles
+2 à 2 qui n'est pas une égalité, mais une inclusion !
+
+**Principe du réordonnancement de BDD:** l'exécution symbolique du **bloc transformé** réordonne le BDD de
+façon à respecter la numérotation: un pére doit avoir un numéro inférieur à
+chacun de ses fils (en l'absence de numéro, on ignore les contraintes
+de numérotation entre ce noeud est ses voisins). Exemple ci-dessous
+avec trois conditions distinctes (pour order c1 < c2 < c3):
+
+    if (c3) { if (c1) {f1} else {f1'} } else { if (c2} {f2} else {f2'} } 
+    
+est réordonné en
+
+    if (c1) { if (c2) { if (c3) {f1} else {f2} } else { if (c3) {f1} else {f2'} } } 
+       else { if (c2) { if (c3) {f1'} else {f2} } else { if (c3) {f1'} else {f2'} } }
+
+**rem:** on ajoute ici un undefined behavior potentiel à cause l'execution de c2 quand c3 est vrai. 
+Mais si le **bloc d'origine** est simulé par cet état symbolique réordonné, c'est correct. 
+Le bloc transformé a juste supprimé un test inutile...
+
+Bon, à voir si le principe ci-dessus est vraiment utile dans toute sa
+généralité. Pour simplifier, on peut aussi restreindre le
+réordonnancement du BDD aux cas où il n'y a pas de test redondant
+inséré (comme dans l'exemple initial).
+
+**Version simplifiée: comparaison des BDD sans réordonnancement des conditions**
+
+Dans un premier temps (jusqu'à ce qu'on trouve une optimisation où ça pourrait être utile): pas de réordonnacement des BDD.
+On autorise juste le BDD du bloc transformé à supprimer des conditions par rapport au bloc d'origine.
+Autrement dit, dans la comparaison récursive de `{if (c) BDD1 BDD2}` avec `{if (c') BDD1' BDD2}'`:
+
+- soit `c=c'` et on compare récursivement `BDD1` avec `BDD1'` et `BDD2` avec `BDD2'`.
+- soit `c<>c'` et  on compare récursivement `BDD1` et `BDD2` avec `{if (c') BDD1' BDD2'}`
+
+Ce deuxième cas correspond au fait que le test sur `c` dans le bloc d'origine était inutile!
+
+### Propagation de valeurs symbolique de conditions (et élimination de condition) pendant l'execution symbolique
+
+L'exécution symbolique se propageant en "avant", on peut propager les valeurs des conditions symboliques, qu'on peut utiliser pour éliminer des conditions redondantes 
+(et donc limiter l'explosion du nombre de chemin).
+
+Pour rendre ce mécanisme efficace et puissant, on peut guider ce mécanisme de propagation/élimination avec des annotations introduites par les oracles.
+
+- une annotation "bind_to x" qui indique de mémoriser la valeur (soit "true" soit "false" suivant la branche) de la condition symbolique avec le nom "x"
+- une annotation "eval_to b proof" qui indique que la condition s'évalue sur la constante "b", ce qui est prouvable avec la preuve "proof".
+
+Ici on peut imaginer un langage plus ou moins compliqué pour prouver l'évaluation des conditions. La version la plus simple:
+
+- "eq(x)"  dit simplement que la condition symbolique est syntaxiquement égale celle appelée "x".
+- "eqnot(x)" dit que c'est la négation.
+
+Dans le cas général, on peut introduire tout un système de réécriture pour éliminer les conditions.
+
+En fait, il serait sans doute intéressant de mettre en place un
+"système de réécriture guidé par oracle" pour toutes les instructions
+BTL.  Ça permet de concilier "puissance" de l'exécution symbolique et
+"efficacité". L'exécution symbolique va pouvoir éventuellement faire
+des réécritures compliquées, mais uniquement quand c'est nécessaire.
+
+**Exemple: une "if-conversion" généralisée**
+On aimerait montrer que le bloc d'origine:
+
+    if (c) {
+        x1 = e1
+        x2 = e2
+        y = e
+        x3 = e3
+    } else {
+        x3 = e3'
+        z = e'
+        x1 = e1'
+        x2 = e2'
+    }
+    
+est simulable par le bloc transformé:
+
+    x1 = (c?e1:e1')
+    x2 = (c?e2:e2')
+    x3 = (c?e3:e3')
+    if (c) { y = e } else { z = e' }
+
+une solution: ajouter une régle de réécriture `x = (c?e:e')` en `if (c) { x=e } else {x=e'}` 
+(attention, ce n'est pas une règle de réécriture sur les valeurs
+symboliques, mais sur du code BTL lui-même, avant l'exécution
+symbolique de ce code).
+
+L'exécution symbolique ouvre alors deux branches `c=true` et
+`c=false` sur `x1 = (c?e1:e1')`, puis la propagation/élimination de la
+condition symbolique `c` simplifie les conditionnelles sur `x2`, `x3` et `y`/`z`.
+Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combinatoire).
+
+**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
 
 Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers.