Sea of Nodes : domaines de validité pour valeurs

Télécharger le fichier original (Mémoire de fin d’études)

SEA OF NODES

L’équation définissant une variable x au point de programme n est valide en tout point strictement dominé par n.
La notion d’équation définissant une variable correspond à l’égalité de l’évaluation des membres gauche et droit d’une aﬀectation avec les valeurs des variables dans l’environnement au point courant. Par exemple, si x est défini par x 3 en un nœud n, alors en tout point strictement dominé par n, on sait que x = 3. Dans le cas d’une aﬀectation x y + 1 en un nœud n, l’environnement donne des valeurs à x et y telles que x = y + 1 en tout point domminé par n ; par contre, par exemple dans le cas d’une boucle, l’exécution peut repasser par la définition de y et se retrouver dans une zone non dominée par n, auquel cas l’équation n’est plus valable, puisque l’environnement donne encore à x la valeur obtenue à partir de la valeur précédente de y.
SSA et blocs de base. SSA est en soi une propriété d’une représentation et celle-ci dispose de flexibilité pour représenter un programme qui la respecte. Par exemple, dans CompCertSSA [22], la représentation utilisée est en fait un simple CFG avec des instructions et des variables, tel que mentionné en fin de section 2.1. Une telle approche dans CompCertSSA a rendu son intégration dans la chaîne de CompCert plus aisée, puisque plus proche du langage RTL de CompCert (un simple CFG d’instructions avec des variables). Il est cependant possible de représenter la forme SSA à l’aide d’une représentation utilisant des blocs de base et éliminant la notion de variable, confondant un nœud ou instruction avec la variable qu’il définit. C’est l’approche que l’on retrouve par exemple dans LLVM ou Go.

Sea of Nodes

La représentation qui va nous occuper le plus dans ce manuscrit, sur-nommée Sea of Nodes et introduite par Cliﬀ Click dans sa thèse [20], est une continuation des idées décrites dans les deux sections précédentes. Elle est utilisée dans le compilateur HotSpot [37, 53] pour Java, ainsi que dans le projet LibFirm [13]. Le projet Graal [29] utilise une variante de la même représentation qui met l’accent sur les optimisations spéculatives dans un compilateur dynamique pour Java.
Sea of Nodes est une représentation SSA qui pousse le concept des dé-pendances de données plus loin en se libérant de la contrainte qui veut que toute instruction appartienne à un bloc de base ou, plus générale-ment, à un point du CFG. Chaque instruction calculant une valeur est un nœud du graphe dont les entrées sont d’autres nœuds correspondant à des instructions calculant des données. Par exemple, dans le pseudo code
1
2
if (b) {
x – a
20 CHAPITRE 2. CONTEXTE : REPRÉSENTATIONS INTERMÉDIAIRES
3 y c + 1
4 }
l’instruction y c + 1 va être représentée par un nœud flottant correspon-dant à une instruction d’addition, avec seulement deux entrées venant des nœuds correspondant à la définition d’une variable c et de la constante 1 (des dépendances de données). On confond donc le nœud représentant une instruction et la variable que l’instruction définit, mais, de plus, on oublie (sauf pour les ϕs) l’appartenance à un bloc particulier. Le branchement conditionnel est représenté par un nœud conditionnel avec deux succes-seurs correspondant au cas true et false, appelés projections, du fait que l’on projette sur une branche ou l’autre. On remarque que l’ordre dans le-quel on définit x et y reste libre. C’est seulement plus tard dans la chaîne de compilation qu’un ordre complet va être décidé sur les instructions, d’abord en les aﬀectant à un bloc particulier, puis en les ordonnant à l’intérieur d’un bloc.
En fait, la représentation Sea of Nodes représente les blocs eux-mêmes par des nœuds, appelés nœuds de région, qui seront connectés par des dépendances aux nœuds traitant du flot de contrôle, comme par exemple des sauts, conditionnels ou non, ainsi que des retours de fonction. Ce-ci simplifie l’écriture de certaines analyses de flot de données, comme la propagation de constantes conditionnelle. Cette dernière profite aussi des nœuds de projection pour la conditionnelle, qui permettent d’éviter d’avoir à attacher de façon ad hoc l’information sur la branche prise au niveau des arcs. Nous verrons aussi que la nature flottante des nœuds de données permet d’écrire une sémantique d’évaluation des nœuds de don-nées avec laquelle il est commode de raisonner. De plus, en introduisant moins de dépendances superflues, certains programmes sémantiquement équivalents, mais syntaxiquement diﬀérents avec une représentation plus séquentielle, deviennent syntaxiquement équivalents : la syntaxe épouse mieux la sémantique. Il s’agit là d’une propriété intéressante pour une approche formelle. Ces sujets sont traités dans les chapitres 4, 5 et leur application à la preuve d’optimisations est abordée dans le chapitre 6.
La représentation Sea of Nodes, adaptée pour raisonner sur les optimi-sations, s’éloigne d’une représentation séquentielle des programmes : à un moment, il faut revenir sur une représentation séquentielle et, donc, comme mentionné plus haut, aﬀecter une région à tous les nœuds flottants, puis reconstruire des blocs de base avec des instructions ordonnées. La première étape, donner à chaque nœud de données une région, par exemple à l’aide de l’algorithme de Global Code Motion dû à Click [19], est le sujet principal du chapitre 7. Une des forces de la représentation Sea of Nodes est de séparer proprement les phases d’optimisation du Global Code Motion : d’une part, cela simplifie l’implémentation et, d’autre part, cela facilite le raisonnement et d’autant plus d’un point de vue formel. La séquentialisation ultérieure des instructions à l’intérieur d’un bloc est mentionée brièvement Il existe des variantes et extensions de SSA dont l’objectif est en général de faciliter certaines analyses plus spécifiques. On passe en revue quelques représentations classiques dans cette section.
En particulier, nous donnons des exemples de représentations comme la forme GSA ou le VSDG, qui font des choix spéciaux au niveau des nœuds et dépendances de contrôle (boucles et conditionnelles), tout en ayant une approche analogue à Sea of Nodes pour ce qui est des dépendances de données.
Nous donnons aussi deux exemples d’extensions (SSI, Array SSA) qui sont essentiellement indépendantes de la méthode choisie pour représenter SSA et donc pourraient a priori être intégrées naturellement dans une représentation inspirée de Sea of Nodes.

Program Dependence Graph

Le Program Dependence Graph [32] (PDG) est une représentation, pas nécessairement SSA, sous forme de graphe qui utilise deux types de dé-pendances. Les dépendances de données correspondent essentiellement à celles que l’on trouve dans Sea of Nodes. Le graphe fait également usage de dépendances de contrôle au sens suivant : un nœud n0 a une dépen-dance de contrôle sur un nœud n si l’exécution ou non de n0 se décide en n (une formulation plus formelle s’exprime en termes de post-dominance). Par exemple, si n a deux branches successeurs (dans le CFG), et que n0 se trouve sur l’une des branches mais pas sur l’autre, on a une telle dépen-dance. Remarquons que ces dépendances de contrôle ne correspondent pas à celles du CFG ; en particulier, un nœud avec un seul successeur n’induit pas de dépendance de contrôle sur son successeur. Notons que le PDG à lui seul ne contient pas l’information suffisante au niveau des points de jonction pour obtenir un modèle d’exécution. Le PDG facilite certaines optimisations comme la détection de parallélisme, ainsi que la modification incrémentale des dépendances de données suite à un déroulage de boucle ou la suppression d’une branche.

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 : noeuds 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 Sea of Nodes : domaines de validité pour valeurs
5.1 Propriété de préservation de valeur
5.1.1 Phi-Dépendances d’un noeud de données
5.1.2 Noeuds Phi et valeur d’un noeud
5.2 Formulation en termes de dominance
5.2.1 Graphe de flot de contrôle
5.2.2 Dominance
5.2.3 Application à la préservation de valeur
5.3 Conclusion
6 Sea of Nodes : optimisations
6.1 Élimination de Zero-Checks redondants
6.1.1 Extension du langage : le noeud ZeroCheck
6.1.2 Critère de redondance
6.1.3 Algorithme de détection de ZeroCheck redondants
6.1.4 Élimination de ZeroCheck : correction sémantique
6.2 Propagation de constantes simple
6.2.1 Analyse de flot de données pour constantes
6.2.2 Monotonie
6.2.3 Algorithme
6.2.4 Conséquences des équations de point fixe .
6.2.5 La transformation et sa spécification formelle
6.2.6 Préservation sémantique
6.3 Propagation conditionnelle de constantes
6.3.1 Analyse
6.3.2 Monotonie et algorithme
6.3.3 Conséquences des équations de point fixe .
6.3.4 Spécification de la transformation
6.3.5 Préservation sémantique
6.4 Conclusion
7 Sea of Nodes : retour au bloc de base
7.1 Retour au bloc de base non ordonné
7.1.1 Sémantique par blocs
7.1.2 Équivalence sémantique
7.2 Séquentialisation des instructions d’un bloc
7.3 Conclusion
8 Destruction SSA : élimination des Phi
8.1 Introduction
8.1.1 Remarques préliminaires
8.1.2 Destruction SSA
8.1.3 Destruction SSA et Vérification
8.1.4 Contributions
8.2 Conventional SSA
8.2.1 Syntaxe abstraite
8.2.2 Sémantique
8.2.3 Définition unique et strictness
8.2.4 Séparation des live-ranges
8.3 Destruction sans coalescing
8.3.1 L’algorithme
8.3.2 Propriétés du renommage de variables
8.3.3 Preuve de correction
8.4 Destruction CSSA avec coalescing
8.4.1 L’algorithme
8.4.2 Non-interférence affinée avec la CSSA-valeur
8.4.3 Propriétés du renommage de variables
8.4.4 Preuve de correction
8.5 Résultats expérimentaux
8.6 Conclusion et travail futur
9 Conclusion et Perspectives
9.1 Conclusion
9.2 Perspectives
9.2.1 Travaux en vue de l’intégration dans un compilateur
vérifié
9.2.2 Extension à d’autres représentations similaires