A simple, verified validator for software pipelining

Abstract : Software pipelining is a loop optimization that overlaps the execution of several iterations of a loop to expose more instruction-level parallelism. It can result in first-class performances characteristics, but at the cost of significant obfuscation of the code, making this optimization difficult to test and debug. In this paper, we present a translation validation algorithm that uses symbolic evaluation to detect semantics discrepancies between a loop and its pipelined version. Our algorithm can be implemented simply and efficiently, is provably sound, and appears to be complete with respect to most modulo scheduling algorithms. A conclusion of this case study is that it is possible and effective to use symbolic evaluation to reason about loop transformations.
Type de document :
Communication dans un congrès
ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. 2010, 〈10.1145/1706299.1706311〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00529836
Contributeur : Xavier Leroy <>
Soumis le : mardi 26 octobre 2010 - 17:02:20
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 12:25:29

Fichier

validation-softpipe.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jean-Baptiste Tristan, Xavier Leroy. A simple, verified validator for software pipelining. ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. 2010, 〈10.1145/1706299.1706311〉. 〈inria-00529836〉

Partager

Métriques

Consultations de la notice

146

Téléchargements de fichiers

144