Dealing with arithmetic overflows in the polyhedral model

Bruno Cuervo Parrino 1, 2 Julien Narboux 2, 3 Eric Violard 2, 4 Nicolas Magaud 2, 3
2 CAMUS - Compilation pour les Architectures MUlti-coeurS
LSIIT - Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection, Inria Nancy - Grand Est
3 IGG
LSIIT - Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection
4 ICPS
LSIIT - Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection
Abstract : The polyhedral model provides techniques to optimize Static Control Programs (SCoP) using some complex transforma- tions which improve data-locality and which can exhibit par- allelism. These advanced transformations are now available in both GCC and LLVM. In this paper, we focus on the cor- rectness of these transformations and in particular on the problem of integer overflows. Indeed, the strength of the polyhedral model is to produce an abstract mathematical representation of a loop nest which allows high-level trans- formations. But this abstract representation is valid only when we ignore the fact that our integers are only machine integers. In this paper, we present a method to deal with this problem of mismatch between the mathematical and concrete representations of loop nests. We assume the exis- tence of polyhedral optimization transformations which are proved to be correct in a world without overflows and we provide a self-verifying compilation function. Rather than verifying the correctness of this function, we use an approach based on a validator, which is a tool that is run by the com- piler after the transformation itself and which confirms that the code produced is equivalent to the original code. As we aim at the formal proof of the validator we implement this validator using the Coq proof assistant as a programming language [4].
Type de document :
Communication dans un congrès
Uday Bondhugula and Vincent Loechner. IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Jan 2012, Paris, France. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00655485
Contributeur : Julien Narboux <>
Soumis le : jeudi 29 décembre 2011 - 15:47:15
Dernière modification le : samedi 13 janvier 2018 - 01:03:10
Document(s) archivé(s) le : lundi 5 décembre 2016 - 05:42:49

Fichier

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

Identifiants

  • HAL Id : hal-00655485, version 1

Collections

Citation

Bruno Cuervo Parrino, Julien Narboux, Eric Violard, Nicolas Magaud. Dealing with arithmetic overflows in the polyhedral model. Uday Bondhugula and Vincent Loechner. IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Jan 2012, Paris, France. 2012. 〈hal-00655485〉

Partager

Métriques

Consultations de la notice

441

Téléchargements de fichiers

158