|
 
|
[BRA10] Formal Verification of Coalescing Graph-Coloring Register Allocation
Conférence Internationale avec comité de lecture : ESOP'10, European Symposium On Programming, Paphos (Chypre), January 2010, pp.145-164, Series LNCS,
motcle:
Résumé:
Iterated Register Coalescing (IRC) is a widely used heuristic for performing register allocation via graph coloring. Many implementations in existing compilers follow (more or less faithfully) the imperative
algorithm published in 1996. Several mistakes have been found in some
of these implementations.
In this paper, we present a formal verification (in Coq) of the whole
IRC algorithm. We detail a specification that can be used as a reference for IRC. We also define the theory of register-interference graphs; we implement a purely functional version of the IRC algorithm, and we prove the total correctness of our implementation. The automatic extraction of our IRC algorithm into Caml yields a program with competitive performance. This work has been integrated into the CompCert verified compiler.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| BRA10, | |||
| title | = | "{Formal Verification of Coalescing Graph-Coloring Register Allocation}", | |
| author | = | " S. Blazy and B. Robillard and A. Appel ", | |
| booktitle | = | "{ESOP'10, European Symposium On Programming, Paphos (Chypre)}", | |
| year | = | 2010, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| pages | = | "145-164", | |
| } | |||
