Introducing non-linear parameters to the polyhedron model

A mathematical model based on polyhedra (the so-called “polyhedron model”) serves as a foundation for model based loop program transformation like automatic parallelization. One of the restrictions present in the current polyhedron model is the requirement that the coefficients of variables must be numeric constants. This has been hindering some recent developments which require parametric coefficients of variables. We show how such non-linear parameters can be introduced in the polyhedron model, using quantifier elimination in the real numbers as our main mathematical tool. We describe two approaches of obtaining algorithms for the generalized model. First, we point out how existing algorithms can be implemented for the generalized model. Quantifier elimination is employed in this approach to simplify arising case distinctions. We give Fourier-Motzkin elimination and the Simplex algorithm as examples of this approach. Second, we show how quantifier elimination can be used to solve some problems directly, e.g., by computing lexicographic maxima. We also demonstrate how to apply our methods to the frequently appearing case of tiling an index space with parametric tile size, and we present some performance results of the generalized algorithms we have implemented.