Automatic Correctness Checking for Affine Constrained Loop Tiling Transformations

Abstract

The growth in speed seen in modern processors over the past couple decades has created a need for programs that carefully manage the data fed to CPUs. Often, it is the case the processors are so fast, the memory used to supply them with information cannot keep up. Advanced iteration space transformations for stencil computations have found clever ways of parallelizing computationally heavy workloads while managing memory bandwidth through methods such as loop tiling, which streamline cache usage. Additionally, these methods offer scalable parallelism with respect to problem size. While automatic transformations for complex loop structures are still being researched, the same mathematical framework for checking the correctness of programmer implemented transformations should naturally enable such automation. This paper offers insight into the literature surrounding the Polyhedral Model, Iteration Space Transformations, and the mathematical background on which they are formed. Later, this paper seeks to motivate an investigation of whether non-symbolically-tiled, parameterized iteration space transformations, such as diamond tiling, can be verified for correctness with existing mathematics and programming techniques.