|
 
|
[Rob11] Vérification formelle et optimisation de l’allocation de registres
Mémoire de Thèse : Soutenue le: 30 October 2011, pp. 180, pp.: Directeur:Eric Soutif , Sandrine Blazy et Catherine DuboisRapporteur 1: Alain Darte, Christine Paulin-Mohring
Rapporteur 2:Dominique de Werra
Membre du jury:Xavier Leroy
Membre du jury:
Membre du jury:, : Vérification formelle et optimisation de l’allocation de registres ,
Mots clés: allocation de registres, coloration de graphe, verification formelle
Résumé:
La prise de conscience générale de l'importance de véri er plus scrupuleusement les grammes a engendré une croissance considérable des efforts de véri fication formelle de programme durant cette dernière décennie. Néanmoins, le ode qu'exé ute l'ordinateur, ou ode exé utable, n'est pas le ode é rit par le développeur, ou ode sour e. La véri ation formelle de ompilateurs est don un omplément indispensable à la véri ation de ode sour e. L'une des tâ hes les plus omplexes de ompilation est l'allo ation de registres. C'est lors de elle- i que le ompilateur dé ide de la façon dont les variables du programme sont sto kées en mémoire durant son exé ution. La mémoire omporte deux types de onteneurs : les registres, zones d'a ès rapide, présents en nombre limité, et la pile, de apa ité supposée su sament importante pour héberger toutes les variables d'un pro- gramme, mais à laquelle l'a ès est bien plus lent. Le but de l'allo ation de registres est de tirer au mieux parti de la rapidité des registres, ar une allo ation de registres de bonne qualité peut onduire à une amélioration signi ative du temps d'exé ution du programme. Le modèle le plus onnu de l'allo ation de registres repose sur la oloration de graphe d'interféren e-a nité. Dans ette thèse, l'ob je tif est double : d'une part véri er formelle- ment des algorithmes onnus d'allo ation de registres par oloration de graphe, et d'autre part dé nir de nouveaux algorithmes optimisants pour ette étape de ompilation. Nous montrons tout d'abord que l'assistant à la preuve Coq est adéquat à la formali- sation d'algorithmes d'allo ation de registres par oloration de graphes. Nous pro édons ainsi à la véri ation formelle en Coq d'un des algorithmes les plus lassiques d'allo- ation de registres par oloration de graphes, l'Iterated Register Coales ing (IRC), et d'une généralisation de elui- i permettant à un utilisateur peu familier du système Coq d'implanter fa ilement sa propre variante de et algorithme au seul prix d'une éventuelle perte d'e a ité algorithmique. Ces formalisations né essitent des ré exions autour de la formalisation des graphes d'interféren e-a nité, de la tradu tion sous forme purement fon tionnelle d'algorithmes impératifs et de l'e a ité algorithmique, la terminaison et la orre tion de ette version fon tionnelle. Notre implantation formellement véri ée de l'IRC a été intégrée à un prototype du ompilateur CompCert. Nous avons ensuite étudié deux représentations intermédiaires de programmes, dont la forme SSA, et exploité leurs propriétés pour proposer de nouvelles appro hes de résolution optimale de la fusion, l'une des optimisations opérées lors de l'allo ation de registres dont l'impa t est le plus fort sur la qualité du ode ompilé. Ces appro hes montrent que des ritères de fusion tenant ompte de paramètres globaux du graphe d'interféren e-a nité, tels que sa largeur d'arbre, ouvrent la voie vers de nouvelles méthodes de résolution potentiellement plus performantes.
Commentaires:
Thèse transverse équipe OC et CPR.
Equipe:
sys
BibTeX
| @phdthesis { | |||
| Rob11, | |||
| title | = | "{Vérification formelle et optimisation de l’allocation de registres }", | |
| author | = | "B. Robillard", | |
| year | = | 2011, | |
| pages | = | "180", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{Thèse transverse équipe OC et CPR. Directeur:Eric Soutif , Sandrine Blazy et Catherine Dubois Rapporteur 1: Alain Darte, Christine Paulin-Mohring Rapporteur 2:Dominique de Werra Membre du jury:Xavier Leroy Membre du jury: Membre du jury:}", | |
| } |
