Vijay S. Menon
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.
- 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).]]Google Scholar
- AMME,W.,DALTON, N., VON RONNE, J., AND FRANZ,M. SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form. In Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation (Snowbird, UT, USA, 2001), pp. 137--147.]] Google ScholarDigital Library
- BILARDI, G., AND PINGALI, K. Algorithms for computing the static single assignment form. J. ACM 50, 3 (2003), 375--425.]] Google ScholarDigital Library
- BODÍK, R., GUPTA, R., AND SARKAR, V. ABCD: Eliminating array bounds checks on demand. In Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation (Vancouver, British Columbia, Canada, 2000), pp. 321--333.]] Google ScholarDigital Library
- BRIGGS,P.,COOPER, K. D., AND SIMPSON, L. T. Value numbering. Software--Practice and Experience 27, 6 (June 1996), 701--724.]] Google ScholarDigital Library
- CHAMBERS, C., PECHTCHANSKI, I., SARKAR,V., SERRANO, M. J., AND SRINIVASAN, H. Dependence analysis for Java. In Proceedings of the 12th International Workshop on Languages and Compilers for Parallel Computing (1999), vol. 1863 of Lecture Notes in Computer Science, pp. 35--52.]] Google ScholarDigital Library
- CHEN, J., AND TARDITI, D. A simple typed intermediate language for object-oriented languages. In Proceedings of the 32nd Annual ACM Symposium on Principles of Programming Languages (Long Beach, CA, USA, Jan. 2005), ACM Press, pp. 38--49.]] Google ScholarDigital Library
- COLBY, C., LEE,P., NECULA, G. C., BLAU,F., PLESKO, M., AND CLINE, K. A certifying compiler for Java. In PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation (New York, NY, USA, 2000), ACM Press, pp. 95--107.]] Google ScholarDigital Library
- COOPER, K. D., SIMPSON,L.T.,AND VICK, C. A. Operator strength reduction. ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 5 (September 2001), 603--625.]] Google ScholarDigital Library
- CRARY, K., AND VANDERWAART, J. An expressive, scalable type theory for certified code. In ACM SIGPLAN International Conference on Functional Programming (Pittsburgh, PA, 2002), pp. 191--205.]] Google ScholarDigital Library
- CYTRON, R., FERRANTE, J., ROSEN, B., WEGMAN, M., AND ZADECK, K. An efficient method of computing static single assignment form. In Proceedings of the Sixteenth Annual ACM Symposium on the Principles of Programming Languages (Austin, TX, Jan. 1989).]] Google ScholarDigital Library
- GLEW, N. An efficient class and object encoding. In Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages (Minneapolis, MN, USA, Oct. 2000), ACM Press, pp. 311--324.]] Google ScholarDigital Library
- GROSSMAN, D., AND MORRISETT, J. G. Scalable certification for typed assembly language. In TIC '00: Selected papers from the Third International Workshop on Types in Compilation (London, UK, 2001), Springer-Verlag, pp. 117--146.]] Google ScholarDigital Library
- GUPTA, M., CHOI, J.-D., AND HIND, M. Optimizing Java programs in the presence of exceptions. In Proceedings of the 14th European Conference on Object-Oriented Programming - ECOOP '00 (Lecture Notes in Computer Science, Vol. 1850) (June 2000), Springer-Verlag, pp. 422--446.]] Google ScholarDigital Library
- IGARASHI, A., PIERCE, B., AND WADLER, P. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 3 (May 2001), 396--560. First appeared in OOPSLA, 1999.]] Google ScholarDigital Library
- KNOOP, J., RÜTHING, O., AND STEFFEN, B. Lazy code motion. In Proceedings of the SIGPLAN '92 Conference on Programming Language Design and Implementation (San Francisco, CA, June 1992).]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- MORRISETT, G., WALKER, D., CRARY, K., AND GLEW, N. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems (TOPLAS) 21, 3 (May 1999), 528--569.]] Google ScholarDigital Library
- NECULA, G. Proof-carrying code. In POPL1997 (New York, New York, January 1997), ACM Press, pp. 106--119.]] Google ScholarDigital Library
- NECULA, G.C., AND LEE, P. The design and implementation of a certifying compiler. In PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation (New York, NY, USA, 1998), ACM Press, pp. 333--344.]] Google ScholarDigital Library
- PUGH, W. The Omega test: A fast and practical integer programming algorithm for dependence analysis. In Proceedings of Supercomputing '91 (Albuquerque, NM, Nov. 1991).]] Google ScholarDigital Library
- SHAO, Z., SAHA, B., TRIFONOV,V., AND PAPASPYROU, N. A type system for certified binaries. In Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages (January 2002), ACM Press, pp. 216--232.]] Google ScholarDigital Library
- VANDERWAART, J. C., DREYER, D. R., PETERSEN, L., CRARY, K., AND HARPER, R. Typed compilation of recursive datatypes. In Proceedings of the TLDI 2003: ACM SIGPLAN International Workshop on Types in Language Design and Implementation (New Orleans, LA, January 2003), pp. 98--108.]] Google ScholarDigital Library
- 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).]]Google Scholar
- WALKER, D., CRARY, K., AND MORISETT, G. Typed memory management via static capabilities. ACM Transactions on Programming Languages and Systems (TOPLAS) 22, 4 (July 2000), 701--771.]] Google ScholarDigital Library
- XI, H., AND HARPER, R. Dependently typed assembly language. In International Conference on Functional Programming (September 2001), pp. 169--180.]] Google ScholarDigital Library
Index Terms
- A verifiable SSA program representation for aggressive compiler optimization
Recommendations
A verifiable SSA program representation for aggressive compiler optimization
Proceedings of the 2006 POPL ConferenceWe 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 ...
QSSA: an SSA-based IR for Quantum computing
CC 2022: Proceedings of the 31st ACM SIGPLAN International Conference on Compiler ConstructionQuantum computing hardware has progressed rapidly. Simultaneously, there has been a proliferation of programming languages and program optimization tools for quantum computing. Existing quantum compilers use intermediate representations (IRs) where ...
An abstract intermediate representation in compilation systems
The design of an intermediate representation is critical to the portability of a compiler and the efficiency of code generation. In order to increase the reusability of compiler components, and to simplify the development process of compilers, the paper ...
Comments