JUCS - Journal of Universal Computer Science 9(3): 248-269, doi: 10.3217/jucs-009-03-0248
An Automatic Verification Technique for Loop and Data Reuse Transformations based on Geometric Modeling of Programs
expand article infoK. C. Shashidhar, Maurice Bruynooghe§, Francky Catthoor, Gerda Janssens§
‡ DESICS Division, IMEC vzw, Kapeldreef 75, B-3001 Heverlee, and Department of Computer Science, Katholieke Universiteit Leuven, Belgium§ Department of Computer Science, Katholieke Universiteit Leuven, Katholieke Universiteit Leuven, Belgium
Open Access
Abstract
Optimizing programs by applying source-to-source transformations is a prevalent practice among programmers. Particularly so, while programming for high-performance and cost-effective embedded systems, where the initial program is subject to a series of transformations to optimize computation and communication. In the context of parallelization and custom memory design, such transformations are applied on the loop structures and index expressions of array variables in the program, more often manually than with a tool, leading to the non-trivial problem of checking their correctness. Applied transformations are semantics preserving if the transformed program is functionally equivalent to the initial program from the input-output point of view. In this work we present an automatic technique based on geometric modeling to formally check the functional equivalence of initial and transformed programs under loop and data reuse transformations. The verification is transformation oblivious needing no information either about the particular transformations that have been applied or the order in which they have been applied. Our technique also provides useful diagnostics to locate the detected errors.
Keywords
transformation verification, program equivalence, program transformations, restructuring compilers, geometric modeling