Mechanizing conventional SSA for a verified destruction with coalescing

Delphine Demange 1 Yon Fernandez de Retana 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Modern optimizing compilers rely on the Static Single Assignment (SSA) form to make optimizations fast and simpler to implement. From a semantic perspective, the SSA form is nowadays fairly well understood, as witnessed by recent advances in the field of formally verified compilers. The destruction of the SSA form, however, remains a difficult problem, even in a non-verified environment. In fact, the out-of-SSA transformation has been revisited, for correctness and performance issues, up until recently. Unsurprisingly, state-of-the-art compiler formalizations thus either completely ignore, only partially handle, or implement naively the SSA destruction. This paper reports on the implementation of such a destruction within a verified compiler. We formally define and prove the properties of the generation of Conventional SSA (CSSA) which make its destruction simple to implement and prove. Second, we implement and prove correct a coalescing destruction of CSSA, à la Boissinot et al., where variables can be coalesced according to a refined notion of interference. This formalization work extends the CompCertSSA compiler, whose correctness proof is mechanized in the Coq proof assistant. Our CSSA-based, coalescing destruction removes, on average , more than 99% of introduced copies, and leads to encouraging results concerning spilling during post-SSA register allocation.
Type de document :
Communication dans un congrès
25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain. Proceedings of the 25th International Conference on Compiler Construction
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-01378393
Contributeur : Yon Fernández de Retana <>
Soumis le : vendredi 14 octobre 2016 - 16:08:53
Dernière modification le : vendredi 16 novembre 2018 - 01:40:17
Document(s) archivé(s) le : samedi 4 février 2017 - 00:30:20

Fichier

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

Identifiants

  • HAL Id : hal-01378393, version 1

Citation

Delphine Demange, Yon Fernandez de Retana. Mechanizing conventional SSA for a verified destruction with coalescing. 25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain. Proceedings of the 25th International Conference on Compiler Construction. 〈hal-01378393〉

Partager

Métriques

Consultations de la notice

514

Téléchargements de fichiers

280