From b03e5a23bbe1370ba0cbb417d81a4505c317da9a Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 11 Jun 2021 15:33:22 +0200 Subject: Roadmap: precision sur le cout de verification des superblocks --- scheduling/BTLroadmap.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'scheduling') 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' -- cgit