Formal Verification of Coalescing Graph-Coloring Register Allocation - 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

Formal Verification of Coalescing Graph-Coloring Register Allocation

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.
Fichier principal
Vignette du fichier
2010ESOP.pdf (258.85 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

inria-00477689 , version 1 (29-04-2010)

Identifiants

  • HAL Id : inria-00477689 , version 1

Citer

Sandrine Blazy, Benoît Robillard, Andrew W. W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. pp.145-164. ⟨inria-00477689⟩
290 Consultations
165 Téléchargements

Partager

Gmail Facebook X LinkedIn More