Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Thursday, October 28, 2010 - 5:11:45 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:26 AM
Long-term archiving on: : Friday, October 26, 2012 - 12:30:31 PM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles