diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-24 09:30:13 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-24 09:30:13 +0200 |
| commit | 6781fad2c0cf9403e761692ce248252f13b4aefe (patch) | |
| tree | 0e522099fc9978577524529436cfc520b38f37a0 /scheduling | |
| parent | 99b1514f31869bc11c4eb89a7a9b46e5fef81881 (diff) | |
| download | compcert-kvx-6781fad2c0cf9403e761692ce248252f13b4aefe.tar.gz compcert-kvx-6781fad2c0cf9403e761692ce248252f13b4aefe.zip | |
update BTLroadmap
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTLroadmap.md | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 23677ba2..3d799235 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -123,9 +123,7 @@ simultanée. **STATUS** -1. See [BTL.fsem] -2. fsem -> cfgsem: fait (ou presque). -3. cfgsem -> fsem: a faire (via verif de liveness). +DONE. ## "Basic" symbolic execution / symbolic simulation @@ -138,10 +136,13 @@ Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem). +- BTL_SEsimuref.v: DONE (raffinement de la notion d'état symbolique) + +- BTL_Schedulerproof: DONE (preuve que les simulations symboliques locales de blocks/blocks garantissent la simulation globale du programme pour BTL.fsem). + **TODO** -1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof). -2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ? +implem du hash-consing. ## Port of RTLpath optimizations to BTL |