Cobalt: A Language for Writing Provably-Sound Compiler
Optimizations
In Electronic Notes in Theoretical Computer Science, 132(1):
5-17, May 2005.
This paper is a short invited contribution overviewing the Cobalt
language. A detailed discussion of Cobalt can be found in our PLDI 2003 paper, and Cobalt's successor
language, called Rhodium, is
described in our POPL 2005 paper.
Sorin Lerner,
Todd Millstein, and
Craig Chambers
We overview the current status and future directions of the Cobalt
project. Cobalt is a domain-specific language for implementing
compiler optimizations as guarded rewrite rules.
Cobalt optimizations operate over a C-like intermediate representation
including unstructured control flow, pointers to local variables and
dynamically allocated memory, and recursive procedures. The design of
Cobalt engenders a natural inductive strategy for proving the
soundness of optimizations. This strategy is fully automated by
requiring an automatic theorem prover
to discharge a small set of simple proof
obligations for each optimization. We
have written a variety of forward and backward intraprocedural
dataflow optimizations in Cobalt, including constant propagation
and folding, branch folding, full and partial redundancy elimination,
full and partial dead assignment elimination, and simple forms of points-to
analysis. The implementation of
our soundness-checking strategy employs the Simplify
automatic theorem prover, and we have used this implementation to
automatically prove the above optimizations correct.
An execution engine for
Cobalt optimizations is implemented as part of the Whirlwind compiler
infrastructure.
[PDF]