From 6781fad2c0cf9403e761692ce248252f13b4aefe Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 24 Jun 2021 09:30:13 +0200 Subject: update BTLroadmap --- scheduling/BTLroadmap.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'scheduling') 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 -- cgit