Formally verifying a compiler: Why? How? How far?

Abstract : Given the complexity and sophistication of code generation and optimization algorithms, and the difficulty of systematically testing a compiler, it is unsurprising that bugs occur in compilers and cause miscompilation: incorrect executable code is silently generated from a correct source program. The formal verification of a compiler is a radical solution to the miscompilation issue. By applying formal methods (program proof) to the compiler itself, compiler verification proves, with mathematical certainty, that the generated executable code behaves exactly as prescribed by the semantics of the source program. Why indulge in compiler verification? Miscompilation bugs are uncommon enough that, for ordinary, non-critical software, they are negligible compared with the bugs already present in the source program. This is no longer true, however, for critical software, as found in aircraft, medical equipment or nuclear plants, for example. There, miscompilation is a concern, which is currently addressed in unsatisfactory ways such as turning all optimizations off. The risk of miscompilation also diminishes the usefulness of formal methods (model checking, static analysis, program proof) applied at the source level: the guarantees so painfully obtained by source-level verification may not extend to the compiled code that actually runs. How to verify a compiler? For every pass, there is a choice between 1- proving its implementation correct once and for all, and 2- leaving the implementation untrusted, but at each run feed its input and output into a validator: a separate algorithm that tries to establish semantic preservation between input and output code, and aborts compilation (or turns the optimization off) if it cannot. If the soundness of the validator is proved once and for all, approach 2 provides soundness guarantees as strong as approach 1, often at reduced proof costs. I will illustrate both approaches on the verification of two compilation passes: register allocation by graph coloring, and software pipelining. How far can compiler verification go? The state of the art is the CompCert compiler, which compiles almost all of the C language to PowerPC, ARM and x86 assembly and has been mechanically verified using the Coq proof assistant. From a compiler standpoint, however, CompCert leaves much room for improvement: the compilation technology used is early 1980's, few optimizations are implemented, and the performance of the compiled code barely matches that of gcc -O1. Much future work remains, in particular on loop optimizations, which raise semantic challenges that call for principled solutions.
Type de document :
Communication dans un congrès
CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, Apr 2011, Chamonix, France. IEEE, <10.1109/CGO.2011.5764668>
Liste complète des métadonnées

https://hal.inria.fr/hal-01091800
Contributeur : Xavier Leroy <>
Soumis le : samedi 6 décembre 2014 - 17:37:41
Dernière modification le : mercredi 7 octobre 2015 - 01:16:37
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:07:39

Fichier

abstract.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Formally verifying a compiler: Why? How? How far?. CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, Apr 2011, Chamonix, France. IEEE, <10.1109/CGO.2011.5764668>. <hal-01091800>

Partager

Métriques

Consultations de
la notice

87

Téléchargements du document

55