diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-29 08:10:07 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-29 08:10:07 +0200 |
| commit | e6a1df51a2a3d29c58d72453355e50a979e86297 (patch) | |
| tree | e5069ca1151967a54417da6c89eb0485985b17dc /scheduling/BTLroadmap.md | |
| parent | 9208b0c21262839184281d9cc3bdf1e6dca7a416 (diff) | |
| download | compcert-kvx-e6a1df51a2a3d29c58d72453355e50a979e86297.tar.gz compcert-kvx-e6a1df51a2a3d29c58d72453355e50a979e86297.zip | |
BTLroadmap: jumptable
Diffstat (limited to 'scheduling/BTLroadmap.md')
| -rw-r--r-- | scheduling/BTLroadmap.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 815aad96..954143c1 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -349,7 +349,7 @@ Extends the symbolic simulation test to support invariants at block entry, inclu **IDEAS** - En pratique, il faudrait affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie. -Une solution possible: calquer Bjumptable sur Bcond (c-a-d autoriser les Bjumptable en milieu de blocs). On pourrait étendre la prédiction de branchement par profiling aux jumptables (par exemple, avoir des superblocks avec des jumptables au milieu). Un autre intérêt: simplifier le support pour des formes SSA partielles (cf. ci-dessous). +Une solution possible: calquer Bjumptable sur Bcond (c-a-d autoriser les Bjumptable en milieu de blocs). On pourrait étendre la prédiction de branchement par profiling aux jumptables (par exemple, avoir des superblocks avec des jumptables au milieu). Un autre intérêt: simplifier (un peu) le support pour des formes SSA partielles (cf. ci-dessous). Ceci dit, ça compliquerait les choses à plein d'endroits (type Coq [iblock] mutuellement inductif avec [list_iblock] pour avoir les bons principes d'inductions, etc) pour des gains minimes en pratiques ? - Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins). |