Technical Report TR564:
Guaranteed Optimization: Proving Nullspace Properties of Compilers
Todd L. Veldhuizen and Andrew Lumsdaine
(Jul 2002), 35 pages pages
[A short verson of the paper is to appear in: Proceedings of the 2002 Static Analysis Symposium (SAS '02) Madrid, Spain, Sept. 17-20, 2002]
- Abstract:
-
Writing performance-critical programs can be frustrating because optimizing compilers for imperative languages tend to be unpredictable. For a subset of optimizations -- those that simplify rather than reorder code -- it would be useful to prove that a compiler reliably performs optimizations. We show that adopting a ``superanalysis'' approach to optimization enables such a proof. By analogy with linear algebra, we define the nullspace of an optimizer as those programs it reduces to the empty program. To span the nullspace, we define rewrite rules that de-optimize programs by introducing abstraction. For a model compiler we prove that any sequence of de-optimizing rewrite rule applications is undone by the optimizer. Thus, we are able to give programmers a clear mental model of what simplifications the compiler is guaranteed to perform, and make progress on the problem of ``abstraction penalty'' in imperative languages. > > languages. > >
- Available as:
-
|
