diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 15:33:22 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 15:33:22 +0200 |
| commit | b03e5a23bbe1370ba0cbb417d81a4505c317da9a (patch) | |
| tree | 4d7b167434cde64c6cf1d0523a426195354ab2a2 /scheduling/BTLroadmap.md | |
| parent | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (diff) | |
| download | compcert-kvx-b03e5a23bbe1370ba0cbb417d81a4505c317da9a.tar.gz compcert-kvx-b03e5a23bbe1370ba0cbb417d81a4505c317da9a.zip | |
Roadmap: precision sur le cout de verification des superblocks
Diffstat (limited to 'scheduling/BTLroadmap.md')
| -rw-r--r-- | scheduling/BTLroadmap.md | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 9dd21be9..23677ba2 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -142,7 +142,6 @@ Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter 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 ? -Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ? ## Port of RTLpath optimizations to BTL @@ -160,6 +159,14 @@ Approche proposée: utiliser un mécanisme de vérification "simple", basée sur Ci-dessous, on liste quelques "techniques" de collaboration oracle/vérificateur pour contrôler l'explosion des chemins. Idée: les conditions comportent une liste d'annotations qui permet le guidage du vérificateur par l'oracle. +**Remarque** déjà sur les superblocs, le test de simulation par +exécution symbolique est quadratique dans le pire cas. Si on a "n" +variables live sur les sorties et "m" sorties, la vérif est en +"n*m". En pratique, le nombre de sorties est limité, notamment à cause +des contraintes pour respecter la structure de superblocs. En RTLpath, +malgré ce coût quadratique théorique dans le pire cas, en pratique, le +vérificateur passe bien à l'échelle sur nos benchmarks. + ### Contrôle des "joins internes" dans le bloc. Si dans le bloc, toute condition a au plus un "predecesseur" (au sens @@ -179,7 +186,7 @@ On considère le bloc BTL ci-dessous (où les `i*` sont des séquences d'instruc if (c2) { i2; goto pc2 } else { i2' } if (c3} { i3; goto pc3 } else { i3'; goto pc3' } -Sur un tel bloc, il n'y a aucun "join interne" (l'exécution symbolique est donc linéaire). +Sur un tel bloc, il n'y a aucun "join interne" (l'exécution symbolique est donc linéaire et le test de simulation quadratique). Mais représenter en RTLpath un tel bloc nécessite au moins 4 blocks (1 superbloc et 3 basic-blocs): i0; c1; i1; c2; i2'; i3'; goto pc3' |