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]
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.]]
[3]
BILARDI, G., AND PINGALI, K. Algorithms for computing the static single assignment form. J. ACM 50, 3 (2003), 375--425.]]
[4]
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.]]
[5]
BRIGGS,P.,COOPER, K. D., AND SIMPSON, L. T. Value numbering. Software--Practice and Experience 27, 6 (June 1996), 701--724.]]
[6]
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.]]
[7]
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.]]
[8]
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.]]
[9]
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.]]
[10]
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.]]
[11]
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).]]
[12]
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.]]
[13]
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.]]
[14]
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.]]
[15]
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.]]
[16]
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).]]
[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]
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.]]
[20]
NECULA, G. Proof-carrying code. In POPL1997 (New York, New York, January 1997), ACM Press, pp. 106--119.]]
[21]
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.]]
[22]
PUGH, W. The Omega test: A fast and practical integer programming algorithm for dependence analysis. In Proceedings of Supercomputing '91 (Albuquerque, NM, Nov. 1991).]]
[23]
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.]]
[24]
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.]]
[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]
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.]]
[27]
XI, H., AND HARPER, R. Dependently typed assembly language. In International Conference on Functional Programming (September 2001), pp. 169--180.]]
Index Terms
- A verifiable SSA program representation for aggressive compiler optimization
Recommendations
A verifiable SSA program representation for aggressive compiler optimization
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2006432 pages
Copyright © 2006 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 January 2006
Published in SIGPLAN Volume 41, Issue 1
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations36Total Citations
- 847Total Downloads
- Downloads (Last 12 months)10
- Downloads (Last 6 weeks)3
Reflects downloads up to 21 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in