Formal verification of translation validators: a case study on instruction scheduling optimizations

ABSTRACT

Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of itssemantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The validators are designed for two instruction scheduling optimizations: list scheduling and trace scheduling.

REFERENCES

• 1: Andrew W. Appel, Modern Compiler Implementation: In ML, Cambridge University Press, New York, NY, 1998
• 2: Clark W. Barret, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. TVOC: A translation validator for optimizing compilers. In Computer Aided Verification, 17th Int. Conf., CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 291--295. Springer, 2005.
• 3: Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and Logic Programming, 8th Int. Symp., FLOPS 2006, volume 3945 of Lecture Notes in Computer Science, pages 114--129. Springer, 2006.
• 4: Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, 2004.
• 5: David Cachera , Thomas Jensen , David Pichardie , Vlad Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, v.342 n.1, p.56-78, 6 September 2005 [doi>10.1016/j.tcs.2005.06.004]
• 6: Coq development team. The Coq proof assistant. Software and documentation available at http://coq.inria.fr/, 1989--2007.
• 7: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 8: John R. Ellis. Bulldog: a compiler for VLSI architectures. ACM Doctoral Dissertation Awards. The MIT Press, 1986.
• 9: Benjamin Goldberg, Lenore Zuck, and Clark Barret. Into the loops: Practical issues in translation validation for optimizing compilers. In Proc. Workshop Compiler Optimization Meets Compiler Verification (COCV 2004), volume 132 of Electronic Notes in Theoretical Computer Science, pages 53--71. Elsevier, 2005.
• 10: Yuqiang Huang, Bruce R. Childers, and Mary Lou Soffa. Catching and identifying bugs in register allocation. In Static Analysis, 13th Int. Symp., SAS 2006, volume 4134 of Lecture Notes in Computer Science, pages 281--300. Springer, 2006.
• 11: Gerwin Klein , Tobias Nipkow, Verified bytecode verifiers, Theoretical Computer Science, v.298 n.3, p.583-626, 11 April 2003 [doi>10.1016/S0304-3975(02)00869-1]
• 12: 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]
• 13: 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]
• 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 et al. The Compcert certified compiler back-end. Development available at http://gallium.inria.fr/~xleroy/ compcert-backend/, 2003--2007.
• 16: Raya Leviathan , Amir Pnueli, Validating software pipelining optimizations, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France [doi>10.1145/581630.581676]
• 17: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 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. International 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: 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
• 22: Emin Gun Sirer and Brian N. Bershad. Testing Java virtual machines. In Proc. Int. Conf. on Software Testing And Review, 1999.
• 23: Martin Strecker. Compiler verification for C0. Technical report, Université Paul Sabatier, Toulouse, April 2005.
• 24: L. Zuck , A. Pnueli , R. Leviathan, Validation of Optimizing Compilers,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001
• 25: Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for translation validation of optimizing compilers. Journal of Universal Computer Science, 9(3):223--247, 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Algorithms, Languages, Verification

Keywords:
scheduling optimizations, the coq proof assistant, translation validation, verified compilers