Copenhagen Programming Language Seminar


Guaranteed Optimization

Todd Veldhuizen,
Chalmers University of Technology, Sweden

Thursday, December 2nd, 15:15-16:00
DIKU, Universitetsparken 1, room N014


Guaranteed Optimization is a new technique for building compilers that have proven guarantees of what optimizations they perform. Such compilers produce programs that are optimal with respect to certain criteria, such as program size or static operation counts. This optimality result is relative to an approximate program quivalence, exact program equivalence being, of course, undecidable. Guaranteed optimization compilers have a well-defined `kernel', which may roughly be thought of as defining what code is evaluated and erased at compile-time (similar to a binding time specification). The kernel is proven to encompass certain `de-optimizing rewrites' that make programs worse. These rewrites define a closure property of the kernel: any amount of de-optimization can be applied to a source program, and the compiler is guaranteed to undo it all in a single pass. By choosing rewrites that capture common patterns of software engineering abstraction, one can construct compilers that reliably reduce the `abstraction penalty' associated with high-level languages. The de-optimizing rewrites give programmers and language designers an intuitive guarantee of what transformations the compiler has been verified to undo.

Scientific host: Neil Jones. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org