Validating register allocation and spilling - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Validating register allocation and spilling

Résumé

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.
Fichier principal
Vignette du fichier
validation-regalloc.pdf (172.01 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00529841 , version 1 (28-10-2010)

Identifiants

Citer

Silvain Rideau, Xavier Leroy. Validating register allocation and spilling. Compiler Construction 2010, Mar 2010, Paphos, Cyprus. pp.224-243, ⟨10.1007/978-3-642-11970-5_13⟩. ⟨inria-00529841⟩
338 Consultations
262 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More