Validating register allocation and spilling

Abstract : Following the translation validation approach to high-assurance compilation, we describe a new algorithm for validating a posteriori the results of a run of register allocation. The algorithm is based on backward dataflow inference of equations between variables, registers and stack locations, and can cope with sophisticated forms of spilling and live range splitting, as well as many forms of architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.
Type de document :
Communication dans un congrès
Compiler Construction 2010, Mar 2010, Paphos, Cyprus. Springer, 6011, pp.224-243, 2010, Lecture Notes in Computer Science; Compiler Construction 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. <10.1007/978-3-642-11970-5_13>
Liste complète des métadonnées

https://hal.inria.fr/inria-00529841
Contributeur : Xavier Leroy <>
Soumis le : jeudi 28 octobre 2010 - 17:11:45
Dernière modification le : jeudi 29 septembre 2016 - 01:24:17
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 12:30:31

Fichier

validation-regalloc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Silvain Rideau, Xavier Leroy. Validating register allocation and spilling. Compiler Construction 2010, Mar 2010, Paphos, Cyprus. Springer, 6011, pp.224-243, 2010, Lecture Notes in Computer Science; Compiler Construction 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. <10.1007/978-3-642-11970-5_13>. <inria-00529841>

Partager

Métriques

Consultations de
la notice

176

Téléchargements du document

119