Proving optimizations correct using parameterized program equivalence

ABSTRACT

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 a language for implementing complex optimizations using many-to-many rewrite rules, and used this language to implement a variety of optimizations including software pipelining, loop unrolling, loop unswitching, loop interchange, and loop fusion. Finally, to demonstrate the effectiveness of PEC, we used our PEC implementation to verify that all the optimizations we implemented in our language preserve program behavior.

REFERENCES

• 1: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 2: David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a data flow analyser in constructive logic. In ESOP, 2004.
• 3: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 4: Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.178-190, January 16-18, 2002, Portland, Oregon
• 5: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 6: Benjamin Goldberg, Lenore Zuck, and Clark Barrett. Into the loops: Practical issues in translation validation for optimizing compilers. Electronic Notes in Theoretical Computer Science, 132(1):53--71, May 2005.
• 7: Joshua D. Guttman , John D. Ramsdell , Mitchell Wand, VLISP: a verified implementation of Scheme, Lisp and Symbolic Computation, v.8 n.1-2, p.5-32, March 1995 [doi>10.1007/BF01128406]
• 8: M. Kauffmann and R.S. Boyer. The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2):27--62, 1995.
• 9: Wayne Kelly , William Pugh, Finding Legal Reordering Transformations Using Mappings, Proceedings of the 7th International Workshop on Languages and Compilers for Parallel Computing, p.107-124, August 08-10, 1994
• 10: Dexter Kozen, Kleene algebra with tests, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.3, p.427-443, May 1997 [doi>10.1145/256167.256195]
• 11: Sudipta Kundu , Sorin Lerner , Rajesh Gupta, Automated refinement checking of concurrent systems, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 12: Sudipta Kundu , Sorin Lerner , Rajesh Gupta, Validating High-Level Synthesis, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_44]
• 13: David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Proving correctness of compiler optimizations by temporal logic, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.283-294, January 16-18, 2002, Portland, Oregon
• 14: Sorin Lerner , Todd Millstein , Craig Chambers, Automatically proving the correctness of compiler optimizations, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 15: Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.364-377, January 12-14, 2005, Long Beach, California, USA
• 16: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 17: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 18: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 19: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 20: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 21: William Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:4--13, 1992.
• 22: Martin Rinard and Darko Marinov. Credible compilation. In Proceedings of the FLoC Workshop Run-Time Result Verification, July 1999.
• 23: Martin C. Rinard , Pedro C. Diniz, Commutativity analysis: a new analysis framework for parallelizing compilers, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.54-67, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 24: Ganesh Sittampalam , Oege de Moor , Ken Friis Larsen, Incremental execution of transformation specifications, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-38, January 14-16, 2004, Venice, Italy
• 25: Bernhard Steffen, Data Flow Analysis as Model Checking, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.346-365, September 24-27, 1991
• 26: Steven W. K. Tjiang , John L. Hennessy, Sharlit—a tool for building optimizers, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.82-93, June 15-19, 1992, San Francisco, California, United States
• 27: Jean-Baptiste Tristan and Xavier Leroy. Verified validation of lazy code motion. In POPL, 2008.
• 28: Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: a case study on instruction scheduling optimizations. In PLDI, 2009.
• 29: Deborah L. Whitfield , Mary Lou Soffa, An approach for exploring code improving transformations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.1053-1084, Nov. 1997 [doi>10.1145/267959.267960]
• 30: Kwangkeun Yi , Williams Ludwell Harrison, III, Automatic generation and management of interprocedural program analyses, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.246-259, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158642]
• 31: William D. Young, A mechanically verified code generator, Journal of Automated Reasoning, v.5 n.4, p.493-518, Dec. 1989
• 32: Lenore Zuck , Amir Pnueli , Benjamin Goldberg , Clark Barrett , Yi Fang , Ying Hu, Translation and Run-Time Validation of Loop Transformations, Formal Methods in System Design, v.27 n.3, p.335-360, November 2005 [doi>10.1007/s10703-005-3402-z]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability; Validation
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Optimization

General Terms:
Languages, Reliability, Verification

Keywords:
compiler optimization, correctness, translation validation