diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:54:03 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:54:03 +0200 |
| commit | 3924865f98f3232e38ef4c1c0464d332de741c12 (patch) | |
| tree | 02f20482664ae0d02a4802cda4c72c99d6713cc1 /scheduling/BTLroadmap.md | |
| parent | d858606e8400e6aab627f4aac5ec33ce9c2c80fe (diff) | |
| download | compcert-kvx-3924865f98f3232e38ef4c1c0464d332de741c12.tar.gz compcert-kvx-3924865f98f3232e38ef4c1c0464d332de741c12.zip | |
update roadmap
Diffstat (limited to 'scheduling/BTLroadmap.md')
| -rw-r--r-- | scheduling/BTLroadmap.md | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 39ea12d0..32d0b365 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -102,7 +102,7 @@ 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... +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). **IMPLEM PLAN** @@ -113,6 +113,9 @@ En fait, pour le test d'exécution symbolique, il semble plus simple de mettre l c'est la correction du "input_regs" qui garantit que la simulation est correct. La preuve devrait normalement être très similaire à RTLpathLivegenproof. +**STATUS** + +1. See [BTL.fsem] (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem) ## "Basic" symbolic execution / symbolic simulation @@ -124,8 +127,12 @@ We will implement a "basic" (e.g without rewriting rules) "less_undef" simulatio **CURRENT STATUS** -- 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. +- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.semantics + +**next steps** +- preservation proof w.r.t BTL.fsem. +- high-level specification of "symbolic simulation" +- ... ## Port of RTLpath optimizations to BTL |