Frameworks supporting the polyhedral model

Use of the polyhedral model (also called the polytope model) within a compiler requires software to represent the objects of this framework (sets of integer-valued points in regions of various spaces) and perform operations upon them (e.g., testing whether the set is empty).
For more detail about the objects and operations in this model, and an example relating the model to the programs being compiled, see the polyhedral model page.
There are many frameworks supporting the polyhedral model. Some of these frameworks use one or more libraries for
performing polyhedral operations. Others, notably Omega, combine everything in a single package.
Some commonly used libraries are the Omega Library (and a more recent fork), piplib, PolyLib, PPL, isl,
the Cloog polyhedral code generator, and the barvinok library for counting integer solutions.
Of these libraries, PolyLib and PPL focus mostly on rational values, while the other libraries focus on integer values.
The polyhedral framework of gcc is called Graphite. Polly provides polyhedral optimizations for LLVM, and R-Stream has had a polyhedral mapper since ca. 2006.
Common strengths.
Polyhedral frameworks are designed to support compilers techniques for analysis and transformation of codes with nested loops, producing exact results for loop nests with affine loop bounds and subscripts ("Static Control Parts" of programs). They can be used to represent and reason about "executions" (iterations) of statements, rather than treating a statement as a single object representing properties of all executions of that statement. Polyhedral frameworks typically also allow the use of symbolic expressions.
Polyhedral frameworks can be used for dependence analysis for arrays, including both traditional alias analysis and more advanced techniques such as the analysis of data flow in arrays or identification of conditional dependencies. They can also be used to represent code transformation, and provide features to generate the transformed code in a high-level language. The transformation and generation systems can typically handle imperfectly nested loops.
An example to contrast polyhedral frameworks with prior work.
To compare the constraint-based polyhedral model to prior approaches such as individual loop transformations and the unimodular approach, consider the question of whether we can parallelize (execute simultaneously) the iterations of following contrived but simple loop:
 for i := 0 to N do
 A(i) := (A(i) + A(N-i))/2
Approaches that cannot represent symbolic terms (such as the loop-invariant quantity N in the loop bound and subscript) cannot reason about dependencies in this loop. They will either conservatively refuse to run it in parallel, or in some cases speculatively run it completely in parallel, determine that this was invalid, and re-execute it sequentially.
Approaches that handle symbolic terms but represent dependencies via direction vectors or distance vectors will determine that the i loop carries a dependence (of unknown distance), since for example when N=10 iteration 0 of the loop writes an array element (A(0)) that will be read in iteration 10 (as A(10-10)) and reads an array element (A(10-0)) that will later be overwritten in iteration 10 (as A(10)). If all we know is that the i loop carries a dependence, we once again cannot safely run it in parallel.
In reality, there are only dependencies from the first N/2 iterations into the last N/2, so we can execute this loop as a sequence of two fully parallel loops (from 0...N/2 and from N/2+1...N). The characterization of this dependence, the analysis of parallelism, and the transformation of the code can be done in terms of the instance-wise information provided by any polyhedral framework.
Instance-wise analysis and transformation allows the polyhedral model to unify additional transformations (such as index set splitting, loop peeling, tiling, loop fusion or fission, and transformation of imperfectly nested loops) with those already unified by the unimodular framework (such as loop interchange, skewing, and reversal of perfectly nested loops). It has also stimulated the development of new transformations, such as Pugh and Rosser's iteration-space slicing (an instance-wise version of program slicing; note that the code was never released with the Omega Library).
A more interesting example.
Authors of polyhedral frameworks have explored the simple 1-dimensional finite difference heat equation stencil calculation expressed by the following pseudocode:
 for t := 0 to T do
 for i := 1 to N-1 do
 new(i) := (A(i-1) + A(i) + A(i) + A(i+1)) * .25 // explicit forward-difference with R = 0.25
 end
 for i := 1 to N-1 do
 A(i) := new(i)
 end
 end
This code confounds many of the transformation systems of the 20th century,
due to the need to optimize an imperfect loop nest.
Polyhedral frameworks can analyze the flow of information among different executions of statements in the loop nest, and transform this code to simultaneously exploit scalable parallelism and scalable locality.
A re-cap here, of the two approaches on this example, might be nice, but for now see the individual papers of Wonnacott, and Sadayappan et al. as well as others who have studied this code using different frameworks, such as Song and Li.
Differences in presentation or vocabulary.
Comparison of work using different frameworks is complicated by both technical differences (discussed later) and differences in vocabulary and presentation.
Examples are provided below to aid in translation:
Classification of dependences.
Polyhedral Frameworks support dependence analysis in a variety of ways,
helping to capture the impact of symbolic terms,
identify conditional dependences,
and separating out the effects of memory aliasing.
The effects of memory aliasing, in particular, have been described in two ways:
many authors distinguish between "true" data dependences (corresponding to actual flow of information) from false dependences arising from memory aliasing or limited precision of dependence analysis.
The Omega Project publications use specific terms to identify specific effects on analysis.
They maintain the traditional distinction of flow-, output-, and anti-dependences,
based on the types of array access (write to read, write to write, or read to write, respectively).
"Dependences" can independently be classified as memory-based or value-based ---
the former corresponds to memory aliasing,
and the latter does not include dependences interrupted by intervening writes.
A "dependence test" may produce information that is exact or approximate,
depending on the nature of the program being analyzed and the algorithms used in the test.
Finally, the results of dependence analysis will be reported in a "dependence abstraction"
that provides a certain degree of precision.
For example, the "dependence relations" produced by the Omega Test,
and the "quasts" produced by the algorithms of Feautrier or Maydan and Lam,
contain precise information (though in different forms) about the loop iterations involved in a dependence.
The results of either test can be converted into the more traditional "dependence vector" form,
but since this abstraction provides less precision,
much of the information about the dependence will be lost.
Both techniques produce exact information for programs with affine control and subscript expressions,
and must approximate for many programs outside this domain (i.e., in the presence of non-affine subscripts such as index arrays).
The original work of Feautrier focused on describing "true" dependences,
which would be referred to as "exact value-based flow dependences" by the Omega Project.
The Omega Project also described the use of their algorithms for value-based output- and anti-dependences, though Feautrier's quasts could presumably be easily adapted to this as well.
Visualization of transformations and tiling.
There are many ways to produce a visual depiction of the process of transforming and tiling an iteration space.
Some authors depict transformations by changing the location of points on the page, essentially aligning the picture with the coordinate axes of the transformed space; in such diagrams, tiles appear as axis-aligned rectangles/rectangular solids containing iterations. Examples of this approach can be found in the publications and transformation-visualization software of Michelle Mills Strout.
Other authors depict different transformations as different wavefronts of execution that move across the points of the original coordinate system at different angles.
In such diagrams, tiles appear as parallelograms/parallelepipeds.
Examples of this approach can be found in the "time-skewing" publications of David G. Wonnacott.
Differences in approach or implementation status.
Some of the libraries have seen more extensive development than the Omega Library in the early 2000s, and in many places has much more sophisticated algorithms. In particular, users have reported good results with the Cloog code generator (both in terms of the code generated, and in terms of ability to control trade-offs when generating code), and with the algorithms for counting integer solutions (Alexander Barvinok's work requires a vertex description of the polytope, which is not supported in the Omega Library).
There are several other points on which the frameworks differ, specifically:
Precision and speed.
Integer programming is NP-complete, and Maydan showed that the problem of checking array aliasing in nested loops with affine bounds and subscripts is equivalent to integer programming; other operations, such as array dataflow analysis, are even more complex (the algorithms of the Omega Library handle the full language of Presburger Arithmetic, which is O(2^2^2^n)). Thus, it is clearly unrealistic to expect exact fast results for arbitrary problems of array aliasing or array data flow, even over the affine domain. Fortunately, many problems fall into a subset of this domain where general algorithms can produce an exact answer in polynomial time.
Outside of this domain, the Omega Library, piplib and isl emphasize the production of an exact result (except in the cases of certain uses of uninterpreted function symbols in Omega), despite the high complexity. In some cases, such as variable elimination ("projection"), PolyLib and PPL primarily use algorithms for the rational domain, and thus produce an approximation of the result for integer variables. It may be the case that this reduces the common experience with the Omega Library in which a minor change to one coefficient can cause a dramatic shift in the response of the library's algorithms.
Polylib has some operations to produce exact results for Z-polyhedra (integer points bounded by polyhedra), but at the time of this writing, significant bugs have been reported. Note that bugs also exist in the Omega Library, including reliance on hardware-supplied integer types and cases of the full Presburger Arithmetic algorithms that were not implemented in the library. Users who need exact results for integer variables may need to be wary with either library.
Barvinok's techniques for counting integer solutions require a description of the vertices (and bounding rays) of the polyhedron, but produce an exact answer in a way that can be far more efficient than the techniques described by Pugh. Barvinok's algorithm is always polynomial in the input size, for fixed dimension of the polytope and fixed degree of weights, whereas the "splintering" in Pugh's algorithm can grow with the coefficient values (and thus exponentially in terms of input size, despite fixed dimension, unless there is some limit on coefficient sizes).
Vertex enumeration.
Polyhedral libraries such as PolyLib and PPL exploit the double description of polyhedra and therefore naturally support
vertex enumeration on (non-parametric) polytopes.
The Omega Library internally performs vertex enumeration during the computation of the convex hull.
PolyLib and isl provide vertex enumeration on parametric polytopes, which is essential for applying Barvinok's algorithm to parametric polytopes.
Indication of an approximate result.
In some parts of a compiler, an approximate result is acceptable in certain cases. For example, when dependence analysis is used to guide loop transformation, it is generally acceptable to use a superset of the true dependencies—this can prevent an optimization but does not allow illegal code transformations. When the Omega Library produces an approximate answer, the answer is appropriately marked as an upper bound (e.g., via "and UNKNOWN") or a lower bound (e.g., via "or UNKNOWN"). Answers not marked this way are exact descriptions of sets of integer-valued points (except in cases of bugs in the software).
Handling nonlinear terms.
When code contains a mixture of affine and non-affine terms, polyhedral libraries can, in principle, be used to produce approximate results, for example by simply omitting such terms when it is safe to do so. In addition to providing a way to flag such approximate results, the Omega Library allows restricted uses of "Uninterpreted Function Symbols" to stand in for any nonlinear term, providing a system that slightly improves the result of dependence analysis and (probably more significantly) provides a language for communication about these terms (to drive other analysis or communication with the programmer). Pugh and Wonnacott discussed a slightly less restricted domain than that allowed in the library, but this was never implemented (a description exists in Wonnacott's dissertation).
Transitive closure operation.
Some kinds of analysis, such as Pugh and Rosser's iteration space slicing, can be most easily stated in terms of the transitive closure of the dependence information. Both the Omega Library and isl provide a transitive closure operation that is exact for many cases that arise in programs with simple dependence patterns. In other cases, the Omega Library produces a subset of the transitive closure, while isl produces a superset.
In the case of the Omega Library, the subset itself may be approximate, resulting in an upper bound (tagged) of a lower bound (not tagged) of the transitive closure. Note that the computation of an exact transitive closure is undecidable.