Parameterized Equivalence Checking is a technique that checks the correctness of compiler optimizations fully automatically and before the compiler is ever run. We do this by adapting traditional translation validation techniques to the setting of once-and-for-all correctness proofs. Thus, instead of checking each instance of an optimization every time it is applied, we check the entire optimization once when the compiler is built. We achieve this generalization by proving the equivalence of a pair of parameterized programs which represent an optimization as a rewrite rule. Our primary advance over previous fully automated techniques is the ability to handle complex loop optimizations that require simultaneously shifting multiple pieces of code.
Publications
-
Proving Optimizations Correct using Parameterized Program Equivalence
PLDI 09: paper, slides
with Sudipta Kundu and Sorin Lerner
PLDI 2009 Talk