Article

A provably sound TAL for back-end optimization

Authors:

Juan Chen,

Dinghao Wu,

Andrew W. Appel,

Hai FangAuthors Info & Claims

PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation

Pages 208 - 219

https://doi.org/10.1145/781131.781155

Published: 09 May 2003 Publication History

Get Access

Abstract

Typed assembly languages provide a way to generate machine-checkable safety proofs for machine-language programs. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for such large calculi. We have designed and implemented a low-level typed assembly language (LTAL) with a semantic model and established its soundness from the model. Compared to existing typed assembly languages, LTAL is more scalable and more secure; it has no macro instructions that hinder low-level optimizations such as instruction scheduling; its type constructors are expressive enough to capture dataflow information, support the compiler's choice of data representations and permit typed position-independent code; and its type-checking algorithm is completely syntax-directed.We have built a prototype system, based on Standard ML of New Jersey, that compiles most of core ML to Sparc code. We explain how we were able to make the untyped back end in SML/NJ preserve types during instruction selection and register allocation, without restricting low-level optimizations and without knowledge of any type system pervading the instruction selector and register allocator.

References

[1]

Amal~J. Ahmed, Andrew~W. Appel, and Roberto Virga. A stratified semantics of general references embeddable in higher-order logic. In 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pages 75--86. IEEE, June 2001.

Digital Library

Google Scholar

[2]

Andrew~W. Appel. Foundational proof-carrying code. In Symposium on Logic in Computer Science (LICS '01), pages 247--258. IEEE, 2001.

Digital Library

Google Scholar

[3]

Andrew~W. Appel and Amy~P. Felty. A semantic model of types and machine instructions for proof-carrying code. In POPL '00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 243--253. ACM Press, January 2000.

Digital Library

Google Scholar

[4]

Andrew~W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657--683, September 2001.

Digital Library

Google Scholar

[5]

Andrew~W. Appel, Neophytos Michael, Aaron Stump, and Roberto Virga. A trustworthy proof checker. In Iliano Cervesato, editor, Foundations of Computer Security workshop, pages 37--48. DIKU, July 2002. diku.dk/publikationer/tekniske.rapporter/2002/02-12.pdf.

Google Scholar

[6]

Andrew~W. Appel and Daniel~C. Wang. JVM TCB: Measurements of the trusted computing base of Java virtual machines. Technical Report CS-TR-647-02, Princeton University, April 2002.

Google Scholar

[7]

Matthias Blume and Andrew~W. Appel. Lambda-splitting: A higher-order approach to cross-module optimizations. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP '97), pages 112--124, New York, June 1997. ACM Press.

Digital Library

Google Scholar

[8]

Juan Chen. A Sound Typed Assembly Language for Real Languages on Real Machines. PhD thesis, Princeton University, 2003. In preparation.

Google Scholar

[9]

Christopher Colby, Peter Lee, George~C. Necula, Fred Blau, Ken Cline, and Mark Plesko. A certifying compiler for Java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '00). ACM Press, June 2000.

Digital Library

Google Scholar

[10]

Karl Crary. Toward a foundational typed assembly language. In POPL '03: The 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, page (to appear). ACM Press, January 2003.

Digital Library

Google Scholar

[11]

Lal George. MLRISC: Customizable and reusable code generators. Technical report, Bell Laboratories, May 1997.

Google Scholar

[12]

Nadeem Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. A syntactic approach to foundational proof-carrying code. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pages 89--100, July 2002.

Digital Library

Google Scholar

[13]

Allen Leung and Lal George. MLRISC Annotations.

Google Scholar

[14]

Neophytos~G. Michael and Andrew~W. Appel. Machine instruction syntax and semantics in higher-order logic. In CADE-17: 17th International Conference on Automated Deduction, pages 7--24. Springer-Verlag, June 2000. LNAI 1831.

Digital Library

Google Scholar

[15]

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 Second ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta, GA, 1999. INRIA Technical Report 0288, March 1999.

Google Scholar

[16]

Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. J. Functional Programming, 12(1):43--88, January 2002.

Digital Library

Google Scholar

[17]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527--568, May 1999.

Digital Library

Google Scholar

[18]

George Necula. Proof-carrying code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119, New York, January 1997. ACM Press.

Digital Library

Google Scholar

[19]

Zhong Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation, June 1997.

Google Scholar

[20]

Kedar~N. Swadi and Andrew~W. Appel. Typed machine language and its semantics. www.cs.princeton.edu/~appel/papers, July 2001.

Google Scholar

[21]

Gang Tan, Kedar Swadi, Dinghao Wu, and Andrew~W. Appel. Construction of a semantic model for a typed assembly language. January 2003.

Google Scholar

[22]

Dinghao Wu, Andrew~W. Appel, and Aaron Stump. Foundational proof checkers with small witnesses. March 2003.

Digital Library

Google Scholar

[23]

Hongwei Xi and Robert Harper. A dependently typed assembly language. In 2001 ACM SIGPLAN International Conference on Functional Programming, pages 169--180. ACM Press, September 2001.

Digital Library

Google Scholar

Cited By

View all

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
Appel A(2011)Verified software toolchainProceedings of the 20th European conference on Programming languages and systems: part of the joint European conferences on theory and practice of software10.5555/1987211.1987212(1-17)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987211.1987212
Show More Cited By

Index Terms

A provably sound TAL for back-end optimization
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Semantic foundations for typed assembly languages

Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably ...
From system F to typed assembly language

We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides ...
A provably sound TAL for back-end optimization

Typed assembly languages provide a way to generate machine-checkable safety proofs for machine-language programs. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for ...

Reviews

Reviewer: Wes Elwood Munsil

"Typed assembly languages provide a way to generate machine-checkable safety proofs for machine-language programs." In this important paper, the authors describe low-level typed assembly language (LTAL), which they have used to implement a compiler for most of the functional language ML accepted by the standard ML of New Jersey (SML/NJ) compiler/interpreter. They provide a detailed comparison of LTAL with other typed assembly languages, notably typed assembly language x86 (TALx86), dependently typed assembly language (DTAL), featherweight typed assembly language (FTAL), and typed assembly language two (TALT). Features of LTAL include: soundness that is readily established from the semantic model; increased scalability and security; absence of macro instructions that hinder low-level optimizations; expressive type constructors that (among other things) permit typed position-independent code to avoid the necessity of a trusted linker; and a syntax-directed type-checking algorithm. LTAL is part of the Foundational Proof-Carrying Code (FPCC) project at Princeton University. The paper is long, but well written and complete. Of particular interest is the description of the ways in which the authors made MLRISC, an untyped generic framework for compiler back ends, support type-preserving transformations. The authors are frank about the current uncompetitive compile times of their implementation, while showing that run times are competitive on two small benchmarks. They clearly discuss the work that remains to be done. One issue of notational confusion is the authors' tendency to use set intersection and union operators to denote logical "and" and "or," as seen in premise 9 (p. 212). Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation

June 2003

360 pages

ISBN:1581136625

DOI:10.1145/781131

General Chair:
Ron Cytron
Washington University, USA
,
Program Chair:
Rajiv Gupta
University of Arizona, USA

ACM SIGPLAN Notices Volume 38, Issue 5
May 2003
349 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/780822
Issue’s Table of Contents

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: 09 May 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI03

Sponsor:

PLDI03: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 9 - 11, 2003

California, San Diego, USA

Acceptance Rates

PLDI '03 Paper Acceptance Rate 28 of 131 submissions, 21%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
483
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)4

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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
Appel A(2011)Verified software toolchainProceedings of the 20th European conference on Programming languages and systems: part of the joint European conferences on theory and practice of software10.5555/1987211.1987212(1-17)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987211.1987212
Appel A(2011)Verified Software ToolchainProgramming Languages and Systems10.1007/978-3-642-19718-5_1(1-17)Online publication date: 2011
https://doi.org/10.1007/978-3-642-19718-5_1
Ahmed AAppel ARichards CSwadi KTan GWang D(2010)Semantic foundations for typed assembly languagesACM Transactions on Programming Languages and Systems10.1145/1709093.170909432:3(1-67)Online publication date: 16-Mar-2010
https://dl.acm.org/doi/10.1145/1709093.1709094
Myreen MGordon MSlind K(2008)Machine-code verification for multiple architecturesProceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design10.5555/1517424.1517444(1-8)Online publication date: 17-Nov-2008
https://dl.acm.org/doi/10.5555/1517424.1517444
Chen JHawblitzel CPerry FEmmi MCondit JCoetzee DPratikaki P(2008)Type-preserving compilation for large-scale optimizing object-oriented compilersACM SIGPLAN Notices10.1145/1379022.137560443:6(183-192)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.1145/1379022.1375604
Chen JHawblitzel CPerry FEmmi MCondit JCoetzee DPratikaki PGupta RAmarasinghe S(2008)Type-preserving compilation for large-scale optimizing object-oriented compilersProceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1375581.1375604(183-192)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.1145/1375581.1375604
Nita MGrossman DChambers C(2008)A theory of platform-dependent low-level softwareACM SIGPLAN Notices10.1145/1328897.132846543:1(209-220)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328897.1328465
Nita MGrossman DChambers CNecula GWadler P(2008)A theory of platform-dependent low-level softwareProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1328438.1328465(209-220)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328438.1328465
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.

Cited By

Index Terms

Recommendations

Semantic foundations for typed assembly languages

From system F to typed assembly language