Home

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.

By neelk at 2007-08-09 14:44 | Implementation | other blogs | 7741 reads

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).

By naasking at Thu, 2007-08-09 16:14 | login or register to post comments

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.

By Jacques Carette at Thu, 2007-08-09 22:43 | login or register to post comments

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

By shahbaz at Thu, 2007-08-09 23:24 | login or register to post comments