Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In POPL 2010: 37th symposium Principles of Programming Languages, pages 83--92. ACM, 2010.

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.

bib | DOI | Local copy | At publisher's site ] Back


This file was generated by bibtex2html 1.98.