diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-02 16:36:34 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-02 16:36:34 +0200 |
commit | 846fe8fcae71c964b635a56a5e7fdf20eb4b85e5 (patch) | |
tree | a15adca77ce8001a198bec0ff648a1d574b962a2 | |
parent | 63d38609a1418ae99474923ecb6f512e23cee8f5 (diff) | |
download | compcert-kvx-846fe8fcae71c964b635a56a5e7fdf20eb4b85e5.tar.gz compcert-kvx-846fe8fcae71c964b635a56a5e7fdf20eb4b85e5.zip |
more implem notes in BTLroadmap
-rw-r--r-- | scheduling/BTLroadmap.md | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 6babf47c..27e74de5 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -25,7 +25,7 @@ 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:** a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes. **CURRENT STATUS** @@ -41,6 +41,8 @@ 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". + ## 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). @@ -54,6 +56,11 @@ NB: this approach through "destroyed registers" and "SVundef" seems more modular 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. + ## 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. |