From 42e887969f126635cb438fcf8b6f8969555b7eb7 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 26 May 2021 13:01:54 +0200 Subject: avancement roadmap --- scheduling/BTLroadmap.md | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) (limited to 'scheduling/BTLroadmap.md') diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 32d0b365..6042803d 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -3,8 +3,8 @@ 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 only info required from oracles: a "dupmap" mapping block entries. -In contrast, the "global" optimizations would require some invariants annotations at block entry (provided by oracles). +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: @@ -16,6 +16,9 @@ Examples of optimizations that we aim to support: 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: @@ -83,7 +86,7 @@ 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. -**Idée** à côté de la sémantique "à la RTL" pour BTL, on pourrait +**Idée_Informelle** à 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èrerait @@ -102,11 +105,21 @@ 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 (précédente) plutôt qu'au début (de la suivante). +**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). On pourrait aussi 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). **IMPLEM PLAN** -1. définir the "functional semantics" of BTL. +1. définir the "functional semantics" of BTL (dans un premier temps, avec uniquement Vundef en sortie de bloc). Rem: en pratique, la "functional semantics" est définie pour être une "concrétisation" de la sémantique symbolique. Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée. 2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). 3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. en gros: on implémente un vérificateur des infos de liveness. @@ -119,11 +132,13 @@ En fait, pour le test d'exécution symbolique, il semble plus simple de mettre l ## "Basic" symbolic execution / symbolic simulation -We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics. +We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. +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é. **IMPLEM NOTE** - use Continuation Passing Style for an easy recursive generation of "all execution paths". +- dans l'etat concret, prévoir un booleen qui indique la valeur symbolique par defaut des registres: deux cas, soit "Input" (valeur initiale du registre), soit "Sundef" (valeur Vundef). **CURRENT STATUS** @@ -334,9 +349,13 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina ## Invariants at block entry -Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. +Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction. + +**IDEAS** -Case-study: support of strength-reduction. +- En pratique, il faudra peut-être 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. + +- 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). ## Support of SSA-optimizations @@ -346,6 +365,4 @@ This should enable to represent SSA-forms in BTL IR, more or less like in MLIR. ## Alias analysis in the symbolic simulation -A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) - - +A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) -- cgit