Formal Verification of Coalescing Graph-Coloring Register Allocation

Abstract : 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.
Type de document :
Communication dans un congrès
Andrew Gordon. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. Springer, 6012, pp.145-164, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00477689
Contributeur : Sandrine Blazy <>
Soumis le : jeudi 29 avril 2010 - 20:59:50
Dernière modification le : mardi 16 janvier 2018 - 15:54:15
Document(s) archivé(s) le : lundi 22 octobre 2012 - 15:32:04

Fichier

2010ESOP.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00477689, version 1

Citation

Sandrine Blazy, Benoît Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. Andrew Gordon. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. Springer, 6012, pp.145-164, 2010, Lecture Notes in Computer Science. 〈inria-00477689〉

Partager

Métriques

Consultations de la notice

322

Téléchargements de fichiers

139