From 840f0a740f3cddf2d6bbb8d89ae686357ed12e00 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 12 May 2021 10:37:54 +0200 Subject: fix roadmap on "Simulation modulo liveness" --- scheduling/BTLroadmap.md | 85 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 61 insertions(+), 24 deletions(-) (limited to 'scheduling/BTLroadmap.md') diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 2f630a72..dde2090c 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -63,37 +63,74 @@ Branch factorization should also be possible in BTL -> RTL pass. Example: revert 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. +## 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. `pre_output_regs`). 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_undef". Ça peut rendre le cadre du test de simulation plus +simple et plus général. + +L'idée de départ: "Extends BTL with the possibility of destroying a +set of registers at each exit (a destroyed register is simply set to +Vundef)" en prouvant une simulation "less_undef" n'est pas assez +générale! Ça n'autorise pas à introduire de "nouveaux" registres dans +le bloc transformé, juste à donner n'importe quelle valeur aux +registres "hors-liveout". + +**Idée corrigée** à côté de la sémantique "à la RTL" pour BTL, on +définit 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è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 +remplace juste cet état par un nouvel état (rs0,m) où dans rs0, tous les registres +sont initialisés à Vundef sauf ceux du `input_regs` qui sont +initialisés comme une copie de "rs". In fine, on applique le +"iblock_step" sur cet état (rs0,m). + +**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. + +**IMPLEM PLAN** + +1. définir the "functional semantics" of BTL. +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. + c'est la correction du "input_regs" qui garantit que la simulation est correct. + La preuve devrait normalement être très similaire à RTLpathLivegenproof. + ## "Basic" symbolic execution / symbolic simulation -IMPLEM PLAN in two steps: +We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics. -1. a very basic version without rewriting rules, and without support for simulation modulo-liveness. +**IMPLEM NOTE** -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). +- use Continuation Passing Style for an easy recursive generation of "all execution paths". +- pour implementer la "functional semantics", il faut changer + légèrement la sémantique du map qui associe une valeur symbolique à + chaque registre. En RTLpath, un registre "absent" de la map était considéré comme positionné à sa valeur initial. + Là, il faudra considérer qu'il vaut Vundef (il y a une valeur symbolique spéciale à ajouter !) **CURRENT STATUS** -- model of symbolic execution in Continuation-Passing Style, with basic "correctness" thm ("completness" not yet done). - -## Simulation modulo liveness - -Extends BTL with the possibility of destroying a set of registers at each exit (a destroyed register is simply set to Vundef). - -We can the provide a "MarkUnused" pass of BTL -> BTL that insert these destructions at each exit using liveness info ! -(NB: the liveness info could be provided by the RTL -> BTL oracle like on RTLpath). - -In the symbolic execution, destroying a register corresponds to associate it SVundef value. - -NB: this approach through "destroyed registers" and "SVundef" seems more modular (thus simpler) and more general than the current approach on RTLpath. - -The proof of "simulation modulo liveness" of a BTL B1 by a BTL B2 will simply corresponds to compose two forward simulations: B1 --> MarkUnused(B1) --> B2. - -**IMPLEM NOTE:** "MarkUnused" checks the correctness of liveness informations while performing its transformation. -It should computes alive register from block entry, by forward proceeding of "internal instructions" (like in RTLPathLivegen). -When arriving on a final instruction, we marked as "destroyed" all alive registers that are not in the input registers of the exit -Semantically, the destruction of registers happens "in parallel" of the final step of the block. +- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms. +- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t BTL.FunctionalSemantics +(dans une première étape, on peut laisser le "less_undef" de côté: ce sera facile à ajouter quand le cadre sera en place). ## Port of RTLpath optimizations to BTL @@ -301,7 +338,7 @@ Case-study: support of strength-reduction. ## Support of SSA-optimizations -Extends BTL with "register renamings" at exits (in a sense, "register renaming" extends the feature of "register destroying"). +Extends BTL with "register renamings" at exits. This should enable to represent SSA-forms in BTL IR, more or less like in MLIR. -- cgit