## 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

### 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