Fractal Symbolic Analysis Vijay Menon Intel Corporation

Abstract:  Modern compilers perform wholesale restructuring of programs to improve their e ciency. Dependence analysis is the most widely used technique for proving the correctness of such transformations, but it su ers from the limitation that it considers only the memory locations read and written by a statement without considering what is being computed by that statement. Exploiting the semantics of program statements permits more transformations to be proved correct, and is critical for automatic restructuring of codes such as LU with partial pivoting. One approach to exploiting the semantics of program statements is symbolic analysis and comparison of programs. In principle, this technique is very powerful, but in practice, it is intractable for all but the simplest programs. In this paper, we propose a new form of symbolic analysis and comparison of programs which is appropriate for use in restructuring compilers. Fractal symbolic analysis is an approximate symbolic analysis that compares a program and its transformed version by repeatedly simplifying these programs until symbolic analysis becomes tractable while ensuring that equality of the simpli ed programs is su cient to guarantee equality of the original programs. Fractal symbolic analysis combines some of the power of symbolic analysis with the tractability of dependence analysis. We discuss a prototype implementation of fractal symbolic analysis, and show how it can be used to solve the long-open problem of verifying the correctness of transformations required to improve the cache performance of LU factorization with partial pivoting. Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors?compilers and optimization; I.1.2 [Algebraic Manipulation]: Algorithms?analysis of algorithms