Verified validation of lazy code motion

ABSTRACT

Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is an interesting challenge for validation because it is a global optimization that moves code across loops. Consequently, care must be taken not to move computations that may fail before loops that may not terminate. Our validator includes a specific check for anticipability to rule out such incorrect moves. We present a mechanically-checked proof of correctness of the validation algorithm, using the Coq proof assistant. Combining our validator with an unverified implementation of LCM, we obtain a LCM pass that is provably semantics-preserving and was integrated in the CompCert formally verified compiler.

REFERENCES

• 1: Clark W. Barret, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. TVOC: A translation validator for optimizing compilers. In phComputer Aided Verification, 17th Int. Conf., CAV 2005, volume 3576 of Lecture Notes in Computer ScienceLNCS, pages 291---295. Springer, 2005.
• 2: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 3: Rastislav Bodík , Rajiv Gupta , Mary Lou Soffa, Complete removal of redundant expressions, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.1-14, June 17-19, 1998, Montreal, Quebec, Canada
• 4: CoqCoq development team. The Coq proof assistant. Software and documentation available at http://coq.inria.fr/, 1989--2009.
• 5: Sumit Gulwani and George C. Necula. A polynomial-time algorithm for global value numbering. In phStatic Analysis, 11th Int. Symp., SAS 2004, volume 3148 of Lecture Notes in Computer Science, pages 212--227. Springer, 2004.
• 6: Yuqiang Huang, Bruce R. Childers, and Mary Lou Soffa. Catching and identifying bugs in register allocation. In phStatic Analysis, 13th Int. Symp., SAS 2006, volume 4134 of Lecture Notes in Computer Science, pages 281--300. Springer, 2006.
• 7: Aditya Kanade , Amitabha Sanyal , Uday Khedker, A PVS Based Framework for Validating Compiler Optimizations, Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, p.108-117, September 11-15, 2006 [doi>10.1109/SEFM.2006.4]
• 8: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 9: Jens Knoop , Oliver Rüthing , Bernhard Steffen, Lazy code motion, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.224-234, June 15-19, 1992, San Francisco, California, United States
• 10: Jens Knoop , Oliver Rüthing , Bernhard Steffen, Optimal code motion: theory and practice, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.4, p.1117-1155, July 1994 [doi>10.1145/183432.183443]
• 11: Dirk Leinenbach , Wolfgang Paul , Elena Petrova, Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.2-12, September 07-09, 2005 [doi>10.1109/SEFM.2005.51]
• 12: 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
• 13: Xavier Leroy. A formally verified compiler back-end. arXiv:0902.2137 {cs}. Submitted, July 2008.
• 14: 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
• 15: Xavier Leroy , Sandrine Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, v.41 n.1, p.1-31, July 2008 [doi>10.1007/s10817-008-9099-0]
• 16: Xavier Leroy et al. The CompCert verified compiler. Development available at http://compcert.inria.fr, 2004--2009.
• 17: E. Morel , C. Renvoise, Global optimization by suppression of partial redundancies, Communications of the ACM, v.22 n.2, p.96-103, Feb. 1979 [doi>10.1145/359060.359069]
• 18: 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
• 19: Amir Pnueli, Ofer Shtrichman, and Michael Siegel. The code validation tool (CVT) -- automatic verification of a compilation process. phInternational Journal on Software Tools for Technology Transfer, 2: 192--201, 1998a.
• 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: Martin Rinard and Darko Marinov. Credible compilation with pointers. In phWorkshop on Run-Time Result Verification, 1999.
• 22: Xavier Rival, Symbolic transfer function-based approaches to certified compilation, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 14-16, 2004, Venice, Italy
• 23: Bernhard Steffen, Property-Oriented Expansion, Proceedings of the Third International Symposium on Static Analysis, p.22-41, September 24-26, 1996
• 24: Jean-Baptiste Tristan , Xavier Leroy, Formal verification of translation validators: a case study on instruction scheduling optimizations, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 25: Anna Zaks , Amir Pnueli, CoVaC: Compiler Validation by Program Analysis of the Cross-Product, Proceedings of the 15th international symposium on Formal Methods, May 26-30, 2008, Turku, Finland [doi>10.1007/978-3-540-68237-0_5]
• 26: L. Zuck , A. Pnueli , R. Leviathan, Validation of Optimizing Compilers,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001
• 27: Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for translation validation of optimizing compilers. phJournal of Universal Computer Science, 9 (3): 223--247, 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Algorithms, Languages, Verification

Keywords:
lazy code motion, redundancy elimination, the coq proof assistant, translation validation, verified compilers