Soutenance mémoire
Télécharger le fichier pdf d’un mémoire de fin d’études
Allocation de registres par coloration de graphe
Raisonner directement sur le programme RTL pour construire une allocation de registres est délicat en raison des nombreux facteurs à considérer. Il est donc naturel d’avoir recours à des modèles plus condensés et intuitifs. De toutes les modélisations existantes, celle reposant sur la coloration de graphes est la plus connue et la plus étudiée.
Le modèle d’allocation de registres par coloration de graphe d’interférence a été unanimement adopté pour la compilation statique depuis les articles fondateurs de Chaitin au début des années 80 [CAC+81, Cha82]. Ces articles, en plus de montrer comment modéliser l’allocation de registres via la coloration de graphe d’interférence et proposer un algorithme de résolution, prouvent que tout graphe peut être le graphe d’interférence d’un programme.
Ceci implique en particulier que le problème d’allocation de registres est NP-dicile . Il n’existe donc pas d’algorithme polynomial permettant de trouver une solution optimale pour tout graphe, sauf si P = NP. Une résolution heuristique, comme celle proposée par Chaitin, apparaissait donc comme la seule solution viable à l’époque. Cette preuve sera ensuite reprise en détail dans [BDGR06]. Les auteurs reviennent sur les hypothèses trop restrictives eectuées par Chaitin. En relâchant ces hypothèses, le problème d’allocation de registres reste NP-complet dans quasiment tous les cas. Cependant, les causes de complexité apparaissent plus clairement et, contrairement à ce que laisse entendre la preuve de Chaitin, trouver une quelconque coloration valide du graphe n’est pas nécessairement la source principale de cette complexité.
Le problème de coloration de graphe d’interférence permet facilement d’encoder les contraintes de l’allocation de registres. Les sommets du graphe sont les variables du programme, les couleurs sont les registres, et deux sommets sont liés par une arête, appelée interférence, si les variables qu’ils représentent ne peuvent être aectées à un même registre.
Deux sommets liés par une interférence ne doivent donc pas être colorés de la même couleur. Ce modèle a par la suite évolué an de modéliser également les instructions move présentes dans le programme. Celles-ci sont représentées par un second type d’arête, appel ées anités. Ces anités peuvent de plus être pondérées de sorte à représenter par exemple le nombre d’instructions move liant les deux variables. Si les deux sommets liés par une anité se voient attribuer la même couleur, alors toute instruction move les liant pourra être supprimée du code source. On dit dans ce cas que cette anité est satisfaite.
En outre, ce modèle permet de prendre en compte les éventuelles contraintes liées à l’architecture processeur forçant certaines variables à être présentes dans un registre donné.
Il sut pour cela de précolorer le sommet représentatif de la variable contrainte avec la couleur qui représente le registre dans lequel celle-ci doit être placée.
Le problème d’allocation de registres revient alors à chercher la K-coloration du graphe respectant la précoloration qui maximise la somme des poids des anités satisfaites, où K désigne dans tout ce manuscrit le nombre de registres allouables. Interférences et anités obéissent donc à des objectifs antagonistes qu’il faut concilier. Nous ne parlons alors plus de graphe d’interférence, mais de graphe d’interférence-anité. La gure 2.5 présente un exemple de graphe d’interférence-anité, ainsi qu’une allocation de registres valide pour trois registres.
Si le nombre de registres disponibles est insusant, certaines variables ne peuvent être logées en registres ; les sommets correspondants ne sont pas colorés. Le vidage correspond donc à déterminer le plus grand ensemble de sommets possiblement colorable avec K couleurs. La fusion consiste quant à elle à fusionner autant que possible des sommets liés par une anité an que toute coloration leur aecte la même couleur. L’aectation des registres est déterminée par une coloration du graphe.
La simplicité et l’élégance de ce modèle ont engendré de nombreux travaux autour de celui-ci. Certains de ces travaux ont permis de pallier quelques imperfections du modèle, notamment via l’introduction du découpage des durées de vie (ou live-range splitting) [BDEO97, CS98], d’autres de dénir de nouveaux algorithmes plus ns que celui proposé par Chaitin [CH84, BCT94, GA96, PM98, ONI+10], de gérer des contraintes matérielles spéciques à certaines architectures [SE02, SRH04], ou encore de prendre en compte la structure du programme et les fragments de code les plus exécutés [CK91, CDE05, GGP03].
La cinquième composante : le découpage des durées de vie
Le modèle par coloration de graphe déni par Chaitin sur-approxime les contraintes réelles qui pèsent sur l’allocation de registres. Cette vérité éclate dès que l’on remarque que chaque variable est assignée à un et un seul emplacement mémoire durant toute l’exécution. Les méthodes ont donc évolué an de supprimer cette lacune, notamment grâce au découpage des durées de vie [BDEO97, CS98]. Cette technique consiste à copier une variable v en une variable v0 an de les considérer ensuite comme deux variables diérentes plutôt qu’une seule. Il s’agit donc d’une modication du programme et non du procédé de construction du graphe d’interférence-anité. Plus la stratégie de découpage est agressive, i.e. plus elle introduit de copies, et plus la sur-approximation des contraintes est ne [CS98, AG01]. Il est d’ailleurs possible de complètement contrecarrer le défaut du modèle en ajoutant des copies de toutes les variables après chaque instruction, ce qui revient à autoriser chaque variable à changer d’emplacement après chaque instruction. La gure 1.5 illustre un exemple de découpage des durées de vie dans un programme et l’impact de celui-ci sur le graphe d’interférence-anité. Le découpage permet dans ce cas de n’utiliser que deux registres au lieu de trois pour héberger les variables du programme.
L’utilisation du découpage est protable à l’allocation de registres mais possède deux faiblesses. La première réside dans le fait qu’ajouter des copies de variables rend encore plus dicile l’étape de fusion. La seconde est que choisir comment découper les durées de vie pour proter des bienfaits du découpage est encore une question sans réponse dénitive, bien que diverses stratégies ont déjà été proposées.
Allocation de registres et forme SSA
Le concept de découpage souligne l’impact fondamental de la représentation du programme sur la qualité du modèle graphique d’allocation de registres. La représentation intermédiaire sous forme SSA est celle qui a été le plus couronnée de succès pour l’allocation de registres.
Un programme est en forme SSA (ou Single State Assignment Form) [RWZ88, AWZ88, CFR+91, App98b] si chaque variable est dénie textuellement (ou encore, statiquement) une seule fois. Ceci n’interdit cependant pas qu’une variable soit dynamiquement dénie plus d’une fois, comme ce peut être le cas dans le corps d’une boucle. Une telle forme de programme permet à des variables qui partagent le même nom mais ne contiennent jamais les mêmes valeurs d’être clairement identiées comme des entités distinctes.
Nombre de compilateurs optimisants intègrent depuis quelques années une représentation SSA de leur programme, laquelle est propice aux analyses et aux optimisations classiques, comme la propagation de constantes par exemple. Cette forme a donc fait l’objet d’un intérêt particulier ces dernières années et s’est révélée avoir un impact conséquent sur l’allocation de registres. Le premier avantage par rapport à la forme originale du programme est le gain de précision. En eet, si fv1; : : : ; vng sont des variables du programme sous forme SSA qui partageaient un même nom dans le programme original, alors la forme SSA permet à ces variables d’être aectées à diérents emplacements mémoire, contrairement à la forme originale. Plus important encore, le graphe d’interférence d’un programme sous forme SSA appartient à la famille des graphes triangulés [HGG06, HG06, Bou08, Hac07, BVI07], ce qui rend possible la coloration des graphes d’interférence-anité de tels programme avec un nombre minimal de couleurs en temps linéaire [Wes00]. Il devient donc possible de colorer le graphe d’interférence-anité avec K couleurs si une K-coloration existe.
Le vidage demeure néanmoins NP-dicile , mais cette découverte a permis de concevoir des heuristiques dédiées aux programmes sous forme SSA plus ecaces pour le vidage [HGG06, HG06, Hac07] et a mené la recherche en allocation de registres à se concentrer sur l’étape de fusion [And03, GH07, BDR08, BVI07].
Allocation de registres et découpage extrême
Une autre forme de programme intéressante pour l’allocation de registres est la forme élémentaire. Celle-ci consiste à réaliser un découpage des durées de vie après chaque instruction, permettant ainsi de décider de l’emplacement de chaque variable à chaque instant.
Cette démarche a pour la première fois été introduite par Appel et George au sein de leur processus d’optimisation du vidage et de la fusion par programmation linéaire [AG01]. Les auteurs proposent de résoudre le vidage de façon optimale via un programme linéaire et de résoudre ensuite la fusion. Leur approche pour le vidage est instructionnelle, au sens où ils considèrent quelles instructions load et store doivent être générées avant chaque instruction du programme. Ce processus fonctionne bien pour le vidage mais se heurte à la combinatoire du problème de fusion : l’introduction d’un emplacement mémoire et d’une copie par variable et par instruction rend le problème gigantesque. Leurs résultats sont ainsi peu satisfaisants pour la fusion par programmation linéaire et cette dernière est nalement traitée par une heuristique de coloration de graphe. Cependant les graphes qu’ils doivent considérer sont immenses, en raison de la stratégie de découpage extrême que les auteurs ont adoptée.
Ce sont ces travaux qui permettent à Appel et George de déduire que la séparation des phases de vidage et de fusion, alors une nouveauté, ne déprécie que très peu la qualité globale de l’allocation de registres bien qu’une perte de qualité théorique existe, puisque la fusion dépend d’un vidage xé. Ainsi, résoudre de façon optimale la fusion dans les graphes issus de leur méthode de vidage permettrait de construire des allocations de registres d’excellente qualité, en raison de la précision du modèle. C’est en ce sens qu’ils créent l’Optimal Coalescing Challenge [AG00], un jeu de 474 instances de fusion très particulières dont le nombre de sommets varie entre quelques dizaines et près de trente mille, issus de l’intégration de leur algorithme dans le compilateur SML. Les premiers résultats optimaux pour ces instances furent produits par Grund et Hack en 2007 [GH07], via la programmation linéaire. Ils résolvent ainsi 471 des 474 instances, non sans mal pour certaines d’entre elles, et concluent qu’à l’instar des résultats obtenus sur la forme SSA, exploiter les propriétés des instances de l’OCC semble la voie la plus adaptée pour les résoudre plus ecacement.
Trois problèmes, trois solutions
L’impact de la forme du programme sur la résolution de l’allocation suggère deux idées qui sont à la genèse de nos approches de résolution de l’allocation de registres par coloration de graphe. La première est que la méthode de résolution employée doit être orientée par la forme du programme et ses propriétés, puisque la précision du modèle dépend grandement de la forme du programme. Aussi, il est primordial que l’eort de résolution soit en accord avec la représentation du programme : résoudre un problème grossièrement modélisé par des méthodes exponentielles exactes telles que la programmation linéaire est un gâchis ; résoudre grossièrement un modèle très précis en est un autre. Nous n’aborderons donc dans ce manuscrit non pas un problème, celui de l’allocation de registres, mais trois : un pour les programmes quelconques, un pour les programmes sous forme SSA et un pour les programmes sous forme élémentaire. L’étude de ces deux dernières formes est guidée par la seconde idée, laquelle soutient que les anités doivent être considérées plus globalement qu’elles ne le sont actuellement dans la littérature pour arriver à des solutions de meilleure qualité, comme l’ont été les interférences lors des avancées liées à la forme SSA.
Vérification formelle et allocation de registres
Quelques méthodes formelles
Les méthodes formelles regroupent diverses techniques permettant d’assurer des propriétés sur les programmes ayant pour point commun de reposer sur des théories mathématiques.
Le model-checking [Cla08, QS08] consiste à abstraire le système an d’en modéliser et vérier toutes les exécutions possibles. C’est une technique énumérative dont la principale limitation est la taille du modèle. Un compromis doit être trouvé entre la qualité de l’abstraction et son nombre d’états possibles. Plus l’abstraction est ne et plus il y a d’états, ce qui rend dicile la vérication exhaustive des exécutions ; moins l’abstraction est ne et plus il y a de chances que celle-ci introduise des comportements qui ne vérient pas la propriété désirée.
L’analyse statique [CC77] abstrait également le système mais cette fois an de calculer une sur-approximation des exécutions possibles par calcul symbolique. Il est par exemple simple de vérier grâce à l’analyse statique si un programme est susceptible de réaliser un dépassement de tableau, i.e. de demander la valeur d’une case qui n’existe pas dans un tableau, en calculant une sur-approximation des indices de tableau consultés.
La vérication formelle apporte des démonstrations mathématiques, automatiques ou assistées par l’utilisateur, du respect de l’implantation vis-à-vis de la spécication. Par exemple, pour un algorithme de tri de liste, la vérication formelle consiste à écrire l’algorithme de tri et à montrer que la liste retournée est une permutation triée de la liste paramètre. Cette méthode confère un niveau de conance inégalé mais est parfois lourde à mettre en place. Les dicultés que l’on peut rencontrer lors de la vérication formelle d’algorithmes se situent sur trois plans : la spécication, qui doit être dèle au système décrit et peut donc se révéler complexe, l’implantation, qui peut soulever des problèmes d’ecacité algorithmique ou de terminaison, et la preuve, qui doit lier spécication et implantation. Ce tryptique spécication, implantation, preuve, doit être conçu comme une seule entité, en fonction des objectifs que l’on se xe. Désirer une grande ecacité de l’implantation induit en général une preuve complexe. Vouloir simplier la preuve conduit à perdre l’ecacité algorithmique. Un compromis entre la qualité algorithmique du programme et la diculté de sa preuve est donc à dénir avant toute démarche de vérication formelle.
|
Table des matières
1 Introduction
1.1 L’allocation de registres
1.1.1 L’allocation de registres en quelques mots
1.1.2 Quatre composantes de l’allocation de registres
1.1.3 Allocation de registres par coloration de graphe
1.1.4 La cinquième composante : le découpage des durées de vie
1.1.5 Allocation de registres et forme SSA
1.1.6 Allocation de registres et découpage extrême
1.1.7 Trois problèmes, trois solutions
1.2 Vérication formelle et allocation de registres
1.2.1 Quelques méthodes formelles
1.2.2 Le système Coq
1.2.3 Validation a posteriori
1.2.4 Comparaison vérication/validation par l’exemple
1.2.5 Le projet CompCert
1.2.6 Vérication formelle d’algorithmes d’allocation de registres
1.2.7 Vérication formelle d’algorithmes de théorie des graphes
1.3 Contributions
2 Fondements de l’allocation de registres
2.1 Les contraintes de l’allocation de registres
2.1.1 Structure des programmes RTL
2.1.2 Durée de vie et interférences
2.2 Techniques d’allocation de registres
2.2.1 Coloration de graphe d’interférence-anité
2.2.2 Programmation linéaire
2.2.3 Linear scan
2.2.4 Autres travaux
2.3 Allocation de registres par coloration de graphe
2.3.1 Le vidage
2.3.2 Algorithme de vidage de Chaitin
2.3.3 Le découpage des durées de vie
2.3.4 La fusion
2.3.5 IRC
2.3.6 L’algorithme de coupes de Grund et Hack
2.4 Static Single Assignment (SSA)
2.4.1 Forme SSA d’un programme
2.4.2 Les graphes triangulés
2.4.3 Propriété de dominance
2.4.4 Forme SSA et graphes triangulés
2.5 Découpage extrême
2.5.1 Graphes élémentaires
2.5.2 Graphes éclatés
2.6 Bilan
3 Formalisation des graphes d’interférence-anité
3.1 La structure de données
3.1.1 Les sommets
3.1.2 Les arêtes
3.2 Les propriétés de base des graphes d’interférence-anité
3.3 Relation de voisinage et degrés des sommets
3.4 Les fonctions de modication des graphes
3.4.1 Suppression d’un sommet
3.4.2 Suppression des anités incidentes à un sommet
3.4.3 Fusion de deux sommets liés par une anité
3.5 Implantation des graphes d’interférence-anité
3.5.1 Choix d’implantation
3.5.2 La structure de données
3.5.3 Lien entre spécication et implantation
3.6 Fonctions de transformation des graphes
3.6.1 Suppression d’un sommet
3.6.2 Suppression des anités incidentes à un sommet
3.6.3 Fusion de deux sommets liés par une anité
3.7 Bilan
4 Vérication formelle de l’IRC
4.1 Spécication de l’algorithme
4.2 Description de l’implantation
4.2.1 Point de départ
4.2.2 Ensembles de travail et structure dédiée
4.2.3 Description de l’algorithme
4.3 Fonctions de mise à jour de la structure
4.4 Fonctions de mise à jour de la coloration
4.5 Mise à jour des ensembles de travail
4.5.1 Simplication et vidage
4.5.2 Fusion
4.5.3 Gel
4.6 Terminaison
4.7 Correction
4.8 Evaluation expérimentale
4.8.1 Caractéristiques du développement
4.8.2 Implantation dans CompCert
4.8.3 Evaluation du code extrait
4.9 Extensions
4.9.1 Améliorations algorithmiques
4.9.2 Reconstruction
4.10 Bilan
5 Extension de la vérication formelle de l’IRC à une classe d’algorithmes
5.1 Une structure récursive commune
5.2 Description de l’algorithme générique
5.2.1 L’algorithme
5.2.2 Construction des fonctions auxiliaires
5.2.3 Spécication des fonctions de choix de l’utilisateur
5.2.4 Les fonctions de coloration
5.3 Terminaison
5.4 Correction
5.5 Fonctions prédénies
5.5.1 Les fonctions de choix
5.5.2 Les fonctions de coloration
5.6 Exemples
5.6.1 L’algorithme de Chaitin
5.6.2 L’IRC
5.7 Note sur l’optimisation
5.8 Bilan
6 Optimisation de la fusion dans les graphes SSA par programmation linéaire
6.1 De l’impact de la conguration des anités
6.1.1 Preuve de complexité pour K 3 dans les graphes d’interférence bipartis
6.1.2 Preuve de complexité pour K = 2 dans les graphes d’interférence bipartis
6.2 Préliminaires
6.2.1 Séparation de la fusion et de l’aectation aux registres
6.2.2 Largeur d’arbre d’un graphe
6.3 Optimisation dans les (K ? 1)-arbres partiels
6.4 Résolution optimale de la fusion dans les (K ? 1)-arbres partiels
6.4.1 Fusion agressive et multicoupe
6.4.2 Coloration
6.4.3 Résolution
6.5 Extension aux graphes SSA
6.5.1 Les (K ? 1)-arbres partiels
6.5.2 Les graphes SSA
6.6 Résolution optimale dans les graphes SSA
6.6.1 Calcul d’un ensemble compatible optimal par programmation linéaire
6.6.2 Coloration du graphe fusionné
6.6.3 Exemples
6.7 Triangulation des graphes SSA
6.8 Perspectives
6.8.1 Implantation et extensions
6.8.2 Vérication formelle
6.9 Bilan
7 Fusion dans les graphes éclatés par recomposition des durées de vie
7.1 Recomposition des durées de vie
7.1.1 Cliques d’instruction
7.1.2 Couplage asservissant
7.2 Algorithme de recomposition
7.2.1 Détection des cliques parallèles
7.2.2 Algorithme général
7.2.3 Exemple d’application
7.3 Stratégie de fusion optimale
7.3.1 Le processus
7.3.2 Décomposition via les cliques de séparation
7.4 Résultats expérimentaux
7.4.1 Réduction et décomposition
7.4.2 Solutions optimales
7.4.3 Solutions sub-optimales
7.5 Travaux connexes
7.6 Perspectives
7.6.1 Vers une stratégie de découpage idéale
7.6.2 Comparaison des graphes élémentaires et éclatés
7.7 Bilan
8 Conclusions et perspectives
8.1 Contributions
8.1.1 Graphes de Chaitin et vérication formelle
8.1.2 Graphes SSA et approche fondée sur la largeur d’arbre
8.1.3 Graphes éclatés et recomposition
8.1.4 Trois problèmes, trois solutions
8.2 Perspectives
8.2.1 Algorithme prouvé pour architectures à peu de registres
8.2.2 Fusion guidée par la largeur d’arbre
8.2.3 Vérication formelle de compilateurs et forme SSA
8.2.4 Stratégie de découpage idéale
8.2.5 Vérication formelle et optimisation combinatoire
Bibliographie
A Le système Coq
A.1 Le lambda-calcul
A.2 Programmes et preuves
A.3 La construction Inductive
A.4 Les constructions Denition et Fixpoint
A.5 Récursivité non structurelle
A.6 Données complexes et types dépendants
A.7 Preuves
A.8 Architecture des développements
A.8.1 Sections
A.8.2 Modules
Index
Télécharger le rapport complet
