Translation validation for an optimizing compiler

Abstract

We describe a translation validation infrastructure for the GNU C compiler. During the compilation the infrastructure compares the intermediate form of the program before and after each compiler pass and verifies the preservation of semantics. We discuss a general framework that the optimizer can use to communicate to the validator what transformations were performed. Our implementation however does not rely on help from the optimizer and it is quite successful by using instead a few heuristics to detect the transformations that take place.

The main message of this paper is that a practical translation validation infrastructure, able to check the correctness of many of the transformations performed by a realistic compiler, can be implemented with about the effort typically required to implement one compiler pass. We demonstrate this in the context of the GNU C compiler for a number of its optimizations while compiling realistic programs such as the compiler itself or the Linux kernel. We believe that the price of such an infrastructure is small considering the qualitative increase in the ability to isolate compilation errors during compiler testing and maintenance.

References

1. ACCL91 Martin Abadi, Luca Cardelli, P.-L. Curien, and J.-J Ldvy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.
2. C+97 Alessandro Cimatti et al. A provably correct embedded verifier for the certification of safety critical software. In Computer Aided Verification. 9th International Conference. Proceedings, pages 202-213. Springer-Verlag, June 1997.
3. CLN+00 Christopher Colby, Peter Lee, George C. Necula, Fred Blau, and Mark Plesko. A certifying compiler for Java. To appear in Programming Language Design and Implementation, PLDI'00., June 2000.
4. CM75 L.M. Chirica and D. F. Martin. An approach to compiler correctness. A CM SIGPLAN Notices, 10(6):96-103, June 1975.
5. Cyg Cygnus Solutions. DejaGnu Testing Framework. http://www, gnu. org/software / dej agnu / dej agnu. h
6. Dij76 Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
7. Goe97 Wolfgang Goerigk. Towards rigorous compiler implementation verification. In Rudolf Berghammer, editor, Proc. of the 1999' Workshop on Programming Languages and Fundamentals of Programming, pages 118-126, 1997.
8. HPR88 Susan Horowitz, Jan Prins, and Tom Reps. On the adequacy of program dependence graphs for representing programs. In Proceedings of the Fifteenth Annual A CM Symposium on the Principles of Programming Languages, pages 146-157, San Diego, CA, January 1988.
9. Koz98 Dexter Kozen. Efiqcient code certification. Technical Report TR 98-1661, Cornell University, January 1998.
10. MCG+99 Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, 1999.
11. Mic99 Microsoft Corporation. Microsoft Developer Network Library, March 1999.
12. Moo89 J. Strother Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461-492, December 1989.
13. Mor73 F. Lockwood Morris. Advice on structuring compilers and proving them correct. In Proceedings of the First A CM Symposium on Principles of Programming Languages, pages 144-152, 1973.
14. MP67 John McCarthy and James Painter. Correctness of a compiler for arithmetic expressions. In J. T. Schwartz, editor, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967.
15. Nec98 George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Also available as CMU-CS-98-154.
16. NL98 George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In A CM SICPLAN'93 Conference on Programming Language Design and Implementation, pages 333- 344, June 1998.
17. PSS98 Amir Pnueli, M. Siegel, and Eli Singerman. Translation validation. In Bernhard Steffen, editor, Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '93, volume LNCS 1384, pages 151-166. Springer, 1998.
18. Rin99 Martin Rinard. Credible compilers. Technical Report MIT/LCS/TR-776, Massachusetts Institute of Technology, December 1999.
19. RM99 Martin Rinard and Darko Marinov. Credible compilation. In Proceedings of the Run-Time Result Verification Workshop, July 1999.
20. RR89 G. Ramalingam and Thomas Reps. Semantics of program representation graphs. Technical Report CS-TR-89-900, University of Wisconsin, Madison, December 1989.
21. TMC+96 David Tarditi, J. Gregory Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In PLDI'96 Conference on Programming Language Design and Implementation, pages 181-192, May 1996.
22. WCES94 Daniel Weise, Roger F. Crew, Michael Ernst, and Bjarne Steensgaard. Value dependence graphs: representation without taxation. In Proceedings of POPL '954, 21st A CM SICPLAN- SICA CT Symposium on Principles of Programming Languages, pages 297-310, January 1994.
23. WO92 Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In Proceedings of the 1992 A CM Conference on Lisp and Functional Programming, pages 151-160, 1992.
24. YHR92 Wuu Yang, Susan Horowitz, and Thomas Reps. A program integration algorithm that accommodates semantics-preserving transformations. acre Transactions of Software Engineering and Methodology, 1(3):310-354, July 1992.
25. You89 William D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5(4):493-518, December 1989.

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Search methodologies

      • Heuristic function construction

• Software and its engineering

  • Software notations and tools

    • Compilers

  • Software organization and properties

    • Contextual software domains

      • Operating systems

        • Process management