diff options
Diffstat (limited to 'scheduling/BTLroadmap.md')
| -rw-r--r-- | scheduling/BTLroadmap.md | 454 |
1 files changed, 454 insertions, 0 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md new file mode 100644 index 00000000..1514c5d4 --- /dev/null +++ b/scheduling/BTLroadmap.md @@ -0,0 +1,454 @@ +# BTL Development Roadmap + +BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation). +It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event. +The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules. +The main info required from oracles: a "dupmap" mapping block entries (and maybe strategies for controlling path explosion during symbolic execution -- see below). +Moreover, the "global" optimizations would require some invariants annotations at block entry (provided by oracles). + +Examples of optimizations that we aim to support: + + - instruction scheduling + - instruction rewritings (instruction selection) + - branch duplication, "if-lifting" (e.g. side-exit moved up in "traces"). + - strength-reduction + - SSA optimizations + +We sketch below the various kinds of supported optimizations in development order... + +Remark that we may port most of the current optimizations from RTL to BTL (even maybe, register allocation). +However, RTL will probably remain useful for "fine-tuned" duplication that crosses block boundaries (e.g. Duplicate module). + +## 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): + +- during RTL -> BTL (while "building" BTL blocks) +- during BTL -> BTL. Typically, the "if-lifting" à la Justus could be performed/verified in a single pass here ! + +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. + + +**CURRENT STATUS** + +- verifier: implemented and proved w.r.t match_iblock specification. +- Proof: + - BTL -> RTL: done. + - RTL -> BTL: done. +- Oracles: + - BTL -> RTL: TODO. + - RTL -> BTL: started. + +## 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. 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_def". Ça peut rendre le cadre du test de simulation plus +simple et plus général. + +**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL +[BTLmatch.cfgsem], on définit une sémantique [BTL.fsem], où c'est +juste "l'entrée dans un bloc" qui change de sémantique. Intuitivement, +cette 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 pourrait moralement +commencer 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. + +**REM** pour le test d'exécution symbolique, il semble plus adapté de +mettre les Vundef juste à la fin de la transition (précédente) plutôt +qu'au début (de la suivante): c'est d'ailleurs plus proche de la vision SSA. + +En fait, on pourrait faire les deux (dans le détail, ça ne ferait pas +exactement deux fois la même chose: par exemple, quand on sort sur un +call ou un builtin, le résultat du call/builtin n'est jamais dans le +liveout puisqu'il va être écrasé de toute façon pendant la transition, +mais il peut être -- ou pas -- dans le livein de la transition +suivante dans ce même bloc). + +Avoir une initialisation à Vundef en début de bloc permettrait de +faire une analyse des expressions mal initialisées - par exemple à +partir du bloc d'entrée de la fonction. Ça semble complémentaire de +l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une +combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite). + +Donc, dans un premier temps, la BTL.fsem encode/abstrait la notion de +"liveout" pour le test d'exécution symbolique. Les définitions des +deux sémantiques (symbolique et "functional") se font donc en +simultanée. + +**STATUS** + +DONE. + +## "Basic" symbolic execution / symbolic simulation + +We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.fsem. +Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté. + +**STATUS** + +- BTL_SEtheory: DONE + - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem + - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem). + +- BTL_SEsimuref.v: DONE (raffinement de la notion d'état symbolique) + +- BTL_Schedulerproof: DONE (preuve que les simulations symboliques locales de blocks/blocks garantissent la simulation globale du programme pour BTL.fsem). + +**TODO** + +implem du hash-consing. + +## Port of RTLpath optimizations to BTL + +- Generalize superblock scheduling for a notion of "extended-blocks" such that each instruction of a block, except the block entry, has a single predecessor in the block. +- 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. + +**Remarque** déjà sur les superblocs, le test de simulation par +exécution symbolique est quadratique dans le pire cas. Si on a "n" +variables live sur les sorties et "m" sorties, la vérif est en +"n*m". En pratique, le nombre de sorties est limité, notamment à cause +des contraintes pour respecter la structure de superblocs. En RTLpath, +malgré ce coût quadratique théorique dans le pire cas, en pratique, le +vérificateur passe bien à l'échelle sur nos benchmarks. + +### 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 et le test de simulation quadratique). +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) ! + +## Peut-on coder l'égalité modulo liveness comme un cas simple d'invariant symbolique (et faire la vérif de liveneness par execution symbolique) ? + +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** + +- 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. + +Par contre, il faut réintroduire une preuve `lessdef` modulo liveness dans `BTL_Schedulerproof`. + +### 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 + +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 += 1; // i.e. sizeof(int) + 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`. + +**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 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 + +A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) |