Guaranteed Optimization

"Guaranteed Optimization", in Active Libraries and Universal Languages, by Todd L. Veldhuizen. PhD thesis, 2004.

This chapter describes a new technique for designing optimizers that provide proven guarantees of what optimizations they perform. We use rewrite rules to capture common patterns of `adding abstraction' to programs, and develop a proof technique for compilers based on superanalysis (Chapter 2) to prove that any sequence of rule applications is undone in a single step. Such compilers address the problem of `abstraction penalty' --- see Section~1.4.1 --- and offers programmers an intuitive guarantee of what improvements the compiler will perform. We also show that compilers based on this approach find `optimal programs' in a carefully defined sense.

I know it's a little unusual to link to a chapter of a thesis instead of a paper, but on his web page the author said the paper I was planning on linking to ("Guaranteed Optimization: Proving Nullspace Properties of Compilers") had been superceded.

Anyway, the basic idea well illustrates the adage that a small change of POV can yield a lot of insight. Here, Veldhuizen changes the POV of a compiler writer from "optimization" to "de-pessimization", and gets a really nice result: an exact characterization of the specific kinds of inefficient patterns the compiler will eliminate. The value of this kind of predictability can be very large; functional programmers can rely on tail call optimization because we know exactly when the compiler will do the transformation.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I was just reading this

Another interesting insight from the thesis and "Active Libraries": optimizers are theorem provers. This research's focus on eliminating the abstraction penalty is also vitally important if high-level languages ever hope to penetrate into diverse fields (particularly embedded systems).

Most everything is a ``theorem prover''

A lot of computing, and even more so in programming languages, falls into two categories: decision procedures, and property inference. Decision procedures are really constructive proofs (a la Curry-Howard, etc); so in a way they really are a meta-theorem. Property inference, especially via abstract interpretation, subsumes type inference, but also a very large number of activities in a compiler; the interesting parts of the middle of a compiler try to establish that all sorts of ``properties'' hold, so that various transformations can then be applied. As Todd points out, some of these transformations are the inverse of a ``worsening'' transformation, so a ``guaranteed optimization''.

People who use dependent types, especially in Epigram, but also in Concoqtion, really know that PL and theorem-proving are very intimately related. They are not the only ones: part of the formal specification community has long held that ``theories are types'' (for example, see work of Tom Maibaum or Bill Farmer). Of the things that seem that have been more noticed by the mainstream, I would think that ESC/Java is the most prominent.

Meta-Compilation of Language Abstractions

This one might be relevant as well. As far as I can tell, Surana's work allows one to add optimizations in a manner similar to how one might add libraries to an existing compiler.

Meta-Compilation of Language Abstractions