more implem notes in BTLroadmap

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.