Advertisement
Published in:
2010 | OriginalPaper | Chapter
Validating Register Allocation and Spilling
Authors : Silvain Rideau, Xavier Leroy
Published in: Compiler Construction
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.