A verifiable SSA program representation for aggressive compiler optimization

ABSTRACT

We present a verifiable low-level program representation to embed, propagate, and preserve safety information in high perfor-mance compilers for safe languages such as Java and C#. Our representation precisely encodes safety information via static single-assignment (SSA) [11, 3] proof variables that are first-class constructs in the program.We argue that our representation allows a compiler to both (1) express aggressively optimized machine-independent code and (2) leverage existing compiler infrastructure to preserve safety information during optimization. We demonstrate that this approach supports standard compiler optimizations, requires minimal changes to the implementation of those optimizations, and does not artificially impede those optimizations to preserve safety. We also describe a simple type system that formalizes type safety in an SSA-style control-flow graph program representation. Through the types of proof variables, our system enables compositional verification of memory safety in optimized code. Finally, we discuss experiences integrating this representation into the machine-independent global optimizer of STARJIT, a high-performance just-in-time compiler that performs aggressive control-flow, data-flow, and algebraic optimizations and is competitive with top production systems.

REFERENCES

• 1: ADL-TABATABAI, A.-R., BHARADWAJ, J., CHEN, D.-Y., GHU-LOUM, A., MENON, V. S., MURPHY, B. R., SERRANO, M., AND SHPEISMAN, T. The StarJIT compiler: A dynamic compiler for managed runtime environments. Intel Technology Journal 7, 1 (February 2003).
• 2: Wolfram Amme , Niall Dalton , Jeffery von Ronne , Michael Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.137-147, June 2001, Snowbird, Utah, United States
• 3: Gianfranco Bilardi , Keshav Pingali, Algorithms for computing the static single assignment form, Journal of the ACM (JACM), v.50 n.3, p.375-425, May 2003 [doi>10.1145/765568.765573]
• 4: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 5: Preston Briggs , Keith D. Cooper , L. Taylor Simpson, Value numbering, Software—Practice & Experience, v.27 n.6, p.701-724, June 1997 [doi>10.1002/(SICI)1097-024X(199706)27:6<701::AID-SPE104>3.3.CO;2-S]
• 6: Craig Chambers , Igor Pechtchanski , Vivek Sarkar , Mauricio J. Serrano , Harini Srinivasan, Dependence Analysis for Java, Proceedings of the 12th International Workshop on Languages and Compilers for Parallel Computing, p.35-52, August 04-06, 1999
• 7: Juan Chen , David Tarditi, A simple typed intermediate language for object-oriented languages, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-49, January 12-14, 2005, Long Beach, California, USA
• 8: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 9: Keith D. Cooper , L. Taylor Simpson , Christopher A. Vick, Operator strength reduction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.603-625, September 2001 [doi>10.1145/504709.504710]
• 10: Karl Crary , Joseph C. Vanderwaart, An expressive, scalable type theory for certified code, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.191-205, October 04-06, 2002, Pittsburgh, PA, USA
• 11: R. Cytron , J. Ferrante , B. K. Rosen , M. N. Wegman , F. K. Zadeck, An efficient method of computing static single assignment form, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.25-35, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75280]
• 12: Neal Glew, An efficient class and object encoding, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.311-324, October 2000, Minneapolis, Minnesota, United States
• 13: Dan Grossman , J. Gregory Morrisett, Scalable Certification for Typed Assembly Language, Selected papers from the Third International Workshop on Types in Compilation, p.117-146, September 21, 2000
• 14: Manish Gupta , Jong-Deok Choi , Michael Hind, Optimizing Java Programs in the Presence of Exceptions, Proceedings of the 14th European Conference on Object-Oriented Programming, p.422-446, June 12-16, 2000
• 15: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 16: 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
• 17: MENON,V.,GLEW, N., MURPHY, B., MCCREIGHT, A., SHPEIS-MAN, T., ADL-TABATABAI, A.-R., AND PETERSEN, L. A verifiable SSA program representation for aggressive compiler optimization. Tech. Rep. YALEU/DCS/TR-1338, Department of Computer Science, Yale University, 2005.
• 18: MORRISETT, G., CRARY, K., GLEW, N., GROSSMAN, D., SAMUELS, R., SMITH,F.,WALKER, D., WEIRICH, S., AND ZDANCEWIC, S. TALx86: A realistic typed assembly language. In Second ACM SIGPLAN Workshop on Compiler Support for System Software (Atlanta, Georgia, 1999), pp. 25--35. Published as INRIA Technical Report 0288, March, 1999.
• 19: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 20: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 21: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 22: William Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.4-13, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125848]
• 23: Zhong Shao , Bratin Saha , Valery Trifonov , Nikolaos Papaspyrou, A type system for certified binaries, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.217-232, January 16-18, 2002, Portland, Oregon
• 24: Joseph C. Vanderwaart , Derek Dreyer , Leaf Petersen , Karl Crary , Robert Harper , Perry Cheng, Typed compilation of recursive datatypes, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 25: VON RONNE, J., FRANZ, M., DALTON, N., AND AMME, W. Compile time elimination of null- and bounds-checks. In 3rd Workshop on Feedback-Directed and Dynamic Optimization (FDDO-3) (December 2000).
• 26: David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
• 27: Hongwei Xi , Robert Harper, A dependently typed assembly language, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

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

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

General Terms:
Design, Languages, Performance, Reliability, Theory, Verification

Keywords:
SSA formalization, check elimination, intermediate representations, proof variables, safety dependences, type systems, typeability preservation, typed intermediate languages