Fractal Symbolic Analysis

Restructuring compilers use dependence analysis to prove that the meaning of a program is not changed by a transformation. A well-known limitation of dependence analysis is that it examines only the memory locations read and written by a statement, and does not assume any particular interpretation for the operations in that statement.

Exploiting the semantics of these operations enables a wider set of transformations to be used, and is critical for optimizing important codes such as LU factorization with pivoting. In principle, symbolic execution of programs enables the exploitation of such semantic properties, but it is intractable for all but the simplest programs.

We have proposed a new form of symbolic analysis called fractal symbolic analysis for use in restructuring compilers. Fractal symbolic analysis compares a program and its transformed version by repeatedly simplifying these programs until symbolic analysis becomes tractable, ensuring that equality of simplified programs is sufficient to guarantee equality of the original programs. We have shown that fractal symbolic analysis is powerful enough to optimize the cache performance of complex codes like LU factorization with pivoting which cannot be restructured with standard techniques like dependence analysis.

One of the advantages of dependence analysis is that it can be used not just to verify correctness of transformations but also to synthesize transformations using the kind of integer linear programming techniques we discussed in class. At this point, we have some idea of how to use fractal symbolic analysis to prove the correctness of program transformations, but we do not understand how to use it to synthesize transformations. See if you can figure this out. One test of your solution is to see what it does for LU with pivoting. Does it generate the right transformation discussed in our paper? What other codes would benefit from the use of fractal symbolic analysis? Try to think of problems outside the realm of numerical linear algebra!

How to proceed