PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs

Abstract : High-level compiler transformations, especially loop transformations, are widely recognized as critical optimizations to restructure programs to improve data locality and expose parallelism. Guaranteeing the correctness of program transformations is essential, and to date three main approaches have been developed: proof of equivalence of affine programs, matching the execution traces of programs, and checking bit-by-bit equivalence of the outputs of the programs. Each technique suffers from limitations in either the kind of transformations supported, space complexity, or the sensitivity to the testing dataset. In this paper, we take a novel approach addressing all three limitations to provide an automatic bug checker to verify any iteration reordering transformations on affine programs, including non-affine transformations, with space consumption proportional to the original program data, and robust to arbitrary datasets of a given size. We achieve this by exploiting the structure of affine program control- and data-flow to generate at compile-time lightweight checker code to be executed within the transformed program. Experimental results assess the correctness and effectiveness of our method, and its increased coverage over previous approaches.
Type de document :
Communication dans un congrès
Proceedings of the 43nd Annual Symposium on Principles of Programming Languages, 2016, Jan 2016, St Petersburg, United States. ACM
Liste complète des métadonnées

https://hal.inria.fr/hal-01234104
Contributeur : Fabrice Rastello <>
Soumis le : jeudi 26 novembre 2015 - 11:23:09
Dernière modification le : vendredi 6 janvier 2017 - 18:19:02

Identifiants

  • HAL Id : hal-01234104, version 1

Collections

Citation

Wenlei Bao, Krishnamachari Sriram, Louis-Noël Pouchet, Fabrice Rastello, Sadayappan Ponnuswamy. PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs. Proceedings of the 43nd Annual Symposium on Principles of Programming Languages, 2016, Jan 2016, St Petersburg, United States. ACM. 〈hal-01234104〉

Partager

Métriques

Consultations de la notice

281