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 metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00529841
Contributor : Xavier Leroy <>
Submitted on : Thursday, October 28, 2010 - 5:11:45 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, October 26, 2012 - 12:30:31 PM

File

validation-regalloc.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

321

Files downloads

208