Soutenance mémoire
De l’évolution des représentations intermédiaires
Au long des dernières décennies, les langages de programmation ont évolué et se sont éloignés de la représentation binaire de la machine. Ceci rend à la fois les programmes plus portables entre les architectures, plus faciles à écrire, plus sûrs et moins propices aux erreurs ; on fait un meilleur usage du temps du programmeur. On trouve ainsi dans les langages de programmation une multitude d’éléments haut niveau qui font abstraction des détails de la machine, allant de l’allocation de registres, à des systèmes de types variés, en passant par la gestion automatique de la mémoire ou les fonctions de première classe. Cependant, ces avantages ont un coût : la tâche du compilateur consistant à transformer le langage source en du code assembleur s’est complexifiée. Le compilateur est devenu une pierre fondamentale et délicate de la programmation d’aujourd’hui. Plusieurs problématiques émergent. L’absence de bugs dans le compilateur, c’est-à-dire sa correction, devient subtile, demandant des spécifications claires sur les comportements du programme à préserver et beaucoup de minutie à l’heure de l’écriture des transformations. Depuis des décennies, dans les compilateurs industriels, ces spécifications et les invariants à préserver ont reçu un traitement relativement informel ; le lien entre l’implémentation et la spécification est resté dans la tête du programmeur. Malheureusement, cette approche ne donne pas de garanties suffisantes dans le contexte des systèmes critiques, comme l’avionique ou la médecine. C’est pourquoi récemment, avec l’avènement de la compilation vérifiée, en particulier avec CompCert [46], des méthodes alternatives et plus sûres pour assurer la correction du compilateur et la correspondance entre les spécifications et l’implémentation commencent à faire leur apparition.
Par ailleurs, les langages de haut-niveau laissent de plus en plus la tâche d’optimiser le code généré au compilateur. Tout un panorama de techniques et algorithmes d’optimisations s’est développé. On trouvera donc, par exemple, des algorithmes d’allocation de registres de plus en plus sophistiqués, mais aussi de la propagation de constantes, de l’élimination de sous-expressions communes ou des règles de réécritures pour remplacer certaines séquences d’instructions par d’autres équivalentes mais plus efficaces. Notons que toutes ces optimisations ne font qu’ajouter à la complexité du compilateur et rendent donc la question de la correction d’autant plus importante. Il faut, de plus, prouver non seulement la correction des simples optimisations (transformation d’une représentation intermédiaire vers elle même), mais également celle des transformations entre différentes représentations intermédiaires. En effet, le compilateur optimisant utilise normalement plusieurs représentations intermédiaires du programme : en général, on retrouve au moins une représentation intermédiaire reflétant de près la structure du programme source et une représentation non structurée plus simple et plus adaptée aux optimisations .
Le choix d’une représentation intermédiaire adaptée pour représenter un programme est déterminant dans le type d’analyses et d’optimisations que l’on peut réaliser, ainsi que leur simplicité et leur efficacité. Ainsi, là où l’arbre de syntaxe abstraite, proche de la représentation haut-niveau du programme et se reposant sur des abstractions éloignées de la machine, est adapté à des analyses haut-niveau sur les types et sur les erreurs de syntaxe ou sémantique, d’autres représentations sont plus adaptées aux optimisations du code généré. Notamment, le graphe de flot de contrôle (CFG) est une représentation qui se prête bien aux analyses de flot de données [2, 42]. Des représentations plus évoluées, souvent dérivées du CFG, sont actuellement utilisées dans les compilateurs industriels. En particulier, des représentations SSA [25] (Static Single Assignment) sont utilisées, sous diverses formes, dans la majorité des compilateurs industriels optimisants actuels. On retrouve par exemple des représentations SSA dans GCC [64], LLVM [66], HotSpot [37, 53] ou Go [65]. Ces représentations s’intéressent notamment à simplifier et mettre en évidence les liens de dépendance entre instructions, afin de donner plus de flexibilité aux optimisations lorsqu’elles modifient le code. Ceci est particulièrement flagrant dans la représentation utilisée dans HotSpot et due à Cliff Click [21], qui essaie d’éliminer le plus possible de dépendances superflues entre instructions calculant des données.
Vérification et compilation
Durant les deux dernières décennies, la vérification formelle de techniques de compilation réalistes est devenue réalité, inspirée par les travaux effectués sur le compilateur CompCert [46], un compilateur formellement vérifié pour le langage C et qui implémente l’essentiel du standard C90. Un compilateur vérifié se caractérise par la présence d’une preuve formelle, souvent réalisée à l’aide d’un assistant de preuve comme Coq [24], que les comportements du programme sont préservés par la compilation ; en d’autres termes, on a une preuve que la compilation n’introduit pas de bugs. La représentation SSA est arrivée plus tard dans ce panorama avec des efforts indépendants autour de CompCertSSA [4], Vellvm [75, 74], ainsi que les travaux de Blech et al. [8, 7]. Le projet CompCertSSA utilise un validateur complet et vérifié pour la génération du pruned-SSA, fondé sur les frontières de dominance [25]. Le projet Vellvm démontre une version simplifiée de la génération SSA de LLVM utilisant de la promotion de variables allouées sur la pile. Blech et al. étudient l’utilisation de graphes de termes, ainsi que d’ensembles relationnels pour représenter la sémantique d’évaluation d’un bloc de base (basic-block en anglais) tenant compte des dépendances de données et font le lien avec une représentation séquentielle des instructions du bloc ; ils prouvent formellement également une optimisation d’élimination de code mort. Plus récemment, l’algorithme de génération proposé par Braun et al. [12] a été formalisé en Isabelle/HOL [16]. Beaucoup d’efforts ont donc été menés sur la vérification de la génération de SSA en soi, mais du progrès a aussi été réalisé sur la formalisation d’invariants et propriétés utiles de SSA qui facilitent le raisonnement au moment de prouver des optimisations. En particulier, [74, 4, 28] formalisent l’invariant sémantique de strictness, ainsi que du raisonnement équationnel basique et des raisonnements fondés sur la dominance. Ces outils sémantiques permettent par exemple de prouver formellement la correction de la propagation conditionnelle de constantes (SCCP), l’élimination de sous-expressions communes (CSE) à l’aide du Global Value Numbering (GVN) [28], ou la propagation de copies et des micro-optimisations relatives à la mémoire [74].
Contributions
La propriété SSA a donc déjà été étudiée d’un point de vue sémantique sur des représentations en CFG simples, mais le sujet des dépendances entre instructions a été seulement effleuré d’un point de vue formel précédemment. Cette thèse apporte une étude sémantique de transformations de programmes sous forme SSA en utilisant des représentations qui, non seulement intègrent la propriété fondamentale SSA, mais aussi la flexibilité en termes de dépendances de données entre instructions. Les contributions de cette thèse sont les suivantes.
• Nous donnons une sémantique formelle pour une représentation Sea of Nodes, utilisant une sémantique dénotationnelle pour l’évaluation des instructions correspondant à des calculs de données, mais une sémantique petit-pas pour le flot de contrôle entre régions (blocs) du programme qui, elle, est une extension naturelle de ce que l’on peut retrouver dans CompCertSSA [4] ou Vellvm [74].
• Nous mettons en évidence et prouvons une propriété fondamentale sur les graphes Sea of Nodes : pendant l’exécution d’un programme, la valeur calculée par une instruction reste valide dans toutes les régions dominées par le point de définition.
• Nous illustrons cette propriété en prouvant la correction sémantique d’un algorithme efficace de détection et élimination de zero-checks redondants qui opère directement sur l’arbre de dominance du graphe Sea of Nodes.
• Nous prouvons un algorithme de propagation de constantes sur Sea of Nodes qui utilise une analyse creuse de flot de données standard.
• Nous donnons une nouvelle sémantique pour notre forme SSA qui épouse le concept du bloc de base contenant un ensemble non déterministiquement ordonné d’instructions. Nous utilisons cette sémantique pour prouver la correction d’un retour à une représentation plus séquentielle utilisant des blocs de base sous réserve que certaines propriétés de strictness soient vérifiées ; c’est-à-dire que chaque instruction est placée dans un bloc particulier en respectant certaines contraintes de dominance.
• Nous détaillons un travail de destruction vérifiée réaliste d’une représentation SSA séquentialisée, intégré dans le compilateur vérifié CompCertSSA.
Les propriétés sémantiques sur la représentation Sea of Nodes nécessaires à la preuve de l’optimisation d’élimination de zero-checks redondants, ainsi qu’à la preuve de la propagation simple de constantes, ont fait l’objet d’un développement Coq [61, 24], de même que les preuves de préservation sémantique des optimisations elles-mêmes. Les résultats principaux ont fait l’objet d’une publication [27]. La contribution relative à la destruction de SSA a aussi fait l’objet d’un développement Coq, intégré dans le compilateur CompCertSSA développé et prouvé en Coq, ainsi que d’une publication [26].
|
Table des matières
1 Introduction
1.1 De l’évolution des représentations intermédiaires
1.2 Vérification et compilation
1.3 Contributions
1.4 Structure du manuscrit
2 Contexte : représentations intermédiaires
2.1 Introduction
2.2 Bloc de base et dépendances de données
2.3 SSA
2.3.1 Insensibilité au flot
2.3.2 Chaînes use-def
2.4 Sea of Nodes
2.5 Variantes de SSA
2.5.1 Program Dependence Graph
2.5.2 Gated Single Assignment
2.5.3 Value State Dependence Graph
2.5.4 Thorin
2.5.5 Static Single Information
2.5.6 Array SSA
2.6 Conclusion
3 Contexte : compilation vérifiée
3.1 Introduction
3.2 Compilateurs vérifiés
3.3 Préservation sémantique
3.3.1 Techniques de compilation vérifiée
3.3.2 Simulation lock-step
3.4 Travaux en compilation optimisante vérifiée
3.4.1 CompCert
3.4.2 CompCertSSA
3.4.3 Vellvm
3.4.4 Bloc de base et dépendances de données
3.4.5 CakeML
3.4.6 LVC
3.5 Conclusion
4 Sea of Nodes : syntaxe et sémantique
4.1 Syntaxe
4.2 Sémantique
4.2.1 Sémantique dénotationnelle : nœuds de données
4.2.2 Sémantique opérationnelle : évaluation des régions
4.3 Extensions pour notre Sea of Nodes
4.3.1 Mémoire
4.3.2 Appels système
4.3.3 Opérations bloquantes ou fautives
4.4 Conclusion
5 Conclusion
Télécharger le rapport complet
