More Web Proxy on the site http://driver.im/

Article

A verifiable SSA program representation for aggressive compiler optimization

Authors:

Vijay S. Menon,

Brian R. Murphy,

Andrew McCreight,

Tatiana Shpeisman,

Ali-Reza Adl-Tabatabai,

Leaf PetersenAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 397 - 408

https://doi.org/10.1145/1111037.1111072

Published: 11 January 2006 Publication History

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.]]

Digital Library

[3]

BILARDI, G., AND PINGALI, K. Algorithms for computing the static single assignment form. J. ACM 50, 3 (2003), 375--425.]]

Digital Library

[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.]]

Digital Library

[5]

BRIGGS,P.,COOPER, K. D., AND SIMPSON, L. T. Value numbering. Software--Practice and Experience 27, 6 (June 1996), 701--724.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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).]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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).]]

Digital Library

[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.]]

Digital Library

[20]

NECULA, G. Proof-carrying code. In POPL1997 (New York, New York, January 1997), ACM Press, pp. 106--119.]]

Digital Library

[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.]]

Digital Library

[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).]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[27]

XI, H., AND HARPER, R. Dependently typed assembly language. In International Conference on Functional Programming (September 2001), pp. 169--180.]]

Digital Library

Cited By

Larus JRajwar RLarus JRajwar R(2022)Software Transactional MemoryTransactional Memory10.1007/978-3-031-01719-3_3(53-130)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-01719-3_3
Broda SMachiavelo AMoreira NReis R(2020)Guest ColumnACM SIGACT News10.1145/3388392.338840151:1(38-56)Online publication date: 12-Mar-2020
https://dl.acm.org/doi/10.1145/3388392.3388401
Lee SLee JKim BKim KNoh J(2019)Video Extrapolation Using Neighboring FramesACM Transactions on Graphics10.1145/319649238:3(1-13)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3196492
Show More Cited By

Index Terms

A verifiable SSA program representation for aggressive compiler optimization
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. Formal language definitions
2. Theory of computation

Recommendations

A verifiable SSA program representation for aggressive compiler optimization
Proceedings of the 2006 POPL Conference

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 ...
QSSA: an SSA-based IR for Quantum computing
CC 2022: Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction

Quantum 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

cover image ACM Conferences

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
Issue’s Table of Contents

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
847
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Larus JRajwar RLarus JRajwar R(2022)Software Transactional MemoryTransactional Memory10.1007/978-3-031-01719-3_3(53-130)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-01719-3_3
Broda SMachiavelo AMoreira NReis R(2020)Guest ColumnACM SIGACT News10.1145/3388392.338840151:1(38-56)Online publication date: 12-Mar-2020
https://dl.acm.org/doi/10.1145/3388392.3388401
Lee SLee JKim BKim KNoh J(2019)Video Extrapolation Using Neighboring FramesACM Transactions on Graphics10.1145/319649238:3(1-13)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3196492
Haase C(2018)A survival guide to presburger arithmeticACM SIGLOG News10.1145/3242953.32429645:3(67-82)Online publication date: 26-Jul-2018
https://dl.acm.org/doi/10.1145/3242953.3242964
Popov NCosenza BJuurlink BStogov DWu PHack S(2017)Static optimization in PHP 7Proceedings of the 26th International Conference on Compiler Construction10.1145/3033019.3033026(65-75)Online publication date: 5-Feb-2017
https://dl.acm.org/doi/10.1145/3033019.3033026
Barthe GDemange DPichardie D(2014)Formal Verification of an SSA-Based Middle-End for CompCertACM Transactions on Programming Languages and Systems10.1145/257908036:1(1-35)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1145/2579080
Zhao JNagarakatte SMartin MZdancewic S(2013)Formal verification of SSA-based optimizations for LLVMACM SIGPLAN Notices10.1145/2499370.246216448:6(175-186)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462164
Zhao JNagarakatte SMartin MZdancewic SBoehm HFlanagan C(2013)Formal verification of SSA-based optimizations for LLVMProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462164(175-186)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462164
Zhao JNagarakatte SMartin MZdancewic SField JHicks M(2012)Formalizing the LLVM intermediate representation for verified program transformationsProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103709(427-440)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103709
Zhao JNagarakatte SMartin MZdancewic S(2012)Formalizing the LLVM intermediate representation for verified program transformationsACM SIGPLAN Notices10.1145/2103621.210370947:1(427-440)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103709
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents