Automated Soundness Proofs for Dataflow Analyses and Transformations
via Local Rules
Appears in the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL 2005), Long Beach, California, January 12-14, 2005
Sorin Lerner,
Todd Millstein,
Erika Rice, and
Craig Chambers,
We present Rhodium, a new language for writing compiler
optimizations that can be automatically proved sound. Unlike our
previous work on Cobalt, Rhodium expresses optimizations using explicit
dataflow facts manipulated by local propagation and transformation
rules. This new style allows Rhodium optimizations to be mutually
recursively defined, to be automatically composed, to be interpreted
in both flow-sensitive and -insensitive ways, and to be applied
interprocedurally given a separate context-sensitivity strategy, all
while retaining soundness. Rhodium also supports infinite analysis
domains while guaranteeing termination of analysis. We have
implemented a soundness checker for Rhodium and have specified and
automatically proven the soundness of all of Cobalt's optimizations
plus a variety of optimizations not expressible in Cobalt, including
Andersen's points-to analysis, arithmetic-invariant detection,
loop-induction-variable strength reduction, and redundant array load
elimination.
Download: [PDF | PS]