Sciweavers

Share
POPL
2005
ACM

Automated soundness proofs for dataflow analyses and transformations via local rules

10 years 2 months ago
Automated soundness proofs for dataflow analyses and transformations via local rules
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 loa...
Sorin Lerner, Todd D. Millstein, Erika Rice, Craig
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers
Comments (0)
books