Proving optimizations correct using parameterized program equivalence

Translation validation is a technique for checking that, after an optimization has run, the input and output of the optimization are equivalent. Traditionally, translation validation has been used to prove concrete, fully specified programs equivalent. In this paper we present Parameterized Equivalence Checking (PEC), a generalization of translation validation that can prove the equivalence of parameterized programs. A parameterized program is a partially specified program that can represent multiple concrete programs. For example, a parameterized program may contain a section of code whose only known property is that it does not modify certain variables. By proving parameterized programs equivalent, PEC can prove the correctness of transformation rules that represent complex optimizations once and for all, before they are ever run. We implemented our PEC technique in a tool that can establish the equivalence of two parameterized programs. To highlight the power of PEC, we designed ...

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Sudipta Kundu, Zachary Tatlock, Sorin Lerner
• Keywords: Complex Optimizations, Parameterized Programs, PLDI 2009, Programming Languages, Translation Validation