research-article

The essence of compiling with traces

Authors:

Shu-yu Guo,

Jens PalsbergAuthors Info & Claims

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 563 - 574

https://doi.org/10.1145/1926385.1926450

Published: 26 January 2011 Publication History

Get Access

Abstract

The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox's JavaScript engine. A trace-based JIT compiler leverages run-time profiling to optimize frequently-executed paths while enabling the optimized code to ``bail out'' to the original code when the path has been invalidated. This optimization strategy differs from those of other JIT compilers and opens the question of which trace optimizations are sound. In this paper we present a framework for reasoning about the soundness of trace optimizations, and we show that some traditional optimization techniques are sound when used in a trace compiler while others are unsound. The converse is also true: some trace optimizations are sound when used in a traditional compiler while others are unsound. So, traditional and trace optimizations form incomparable sets. Our setting is an imperative calculus for which tracing is explicitly spelled out in the semantics. We define optimization soundness via a notion of bisimulation, and we show that sound optimizations lead to confluence and determinacy of stores.

Supplementary Material

MP4 File (51-mpeg-4.mp4)

Download
499.30 MB

References

[1]

Vasanth Bala, Evelyn Duesterwald, and Sanjeev Banerjia. Dynamo: A transparent dynamic optimization system. In PLDI '00, pages 1--12. ACM, 2000.

Digital Library

Google Scholar

[2]

Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter. SPUR: A trace-based JIT compiler for CIL. In OOPSLA '10, 2010.

Digital Library

Google Scholar

[3]

Michael Bebenita, Mason Chang, Gregor Wagner, Christian Wimmer, Andreas Gal, and Michael Franz. Trace-based compilation in execution environments without interpreters. In PPPJ '10, 2010.

Digital Library

Google Scholar

[4]

Mason Chang, Edwin W. Smith, Rick Reitmaier, Michael Bebenita, Andreas Gal, Christian Wimmer, Brendan Eich, and Michael Franz. Tracing for web 3.0: trace compilation for the next generation web applications. In VEE, pages 71--80, 2009.

Digital Library

Google Scholar

[5]

Joëlle Despeyroux. Proof of translation in natural semantics. In LICS, pages 193--205, 1986.

Google Scholar

[6]

Cormac Flanagan and Matthias Felleisen. The semantics of future and its use in program optimization. In POPL '95, pages 209--220. ACM, 1995.

Digital Library

Google Scholar

[7]

Andreas Gal. Efficient bytecode verification and compilation in a virtual machine. PhD thesis, 2006. Adviser: Michael Franz.

Digital Library

Google Scholar

[8]

Andreas Gal, Brendan Eich, Mike Shaver, David Anderson, David Mandelin, Mohammad R. Haghighat, Blake Kaplan, Graydon Hoare, Boris Zbarsky, Jason Orendorff, Jesse Ruderman, Edwin W. Smith, Rick Reitmaier, Michael Bebenita, Mason Chang, and Michael Franz. Trace-based just-in-time type specialization for dynamic languages. In PLDI '09, pages 465--478. ACM, 2009.

Digital Library

Google Scholar

[9]

A. J. Kfoury, Michael A. Arbib, and Robert N. Moll. A Programming Approach to Computability. Springer-Verlag, 1982.

Digital Library

Google Scholar

[10]

Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL '06, pages 141--152. ACM, 2006.

Digital Library

Google Scholar

[11]

David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. Proving correctness of compiler optimizations by temporal logic. In POPL '02, pages 283--294. ACM, 2002.

Digital Library

Google Scholar

[12]

Sorin Lerner, Todd Millstein, and Craig Chambers. Automatically proving the correctness of compiler optimizations. In PLDI '03, pages 220--231. ACM, 2003.

Digital Library

Google Scholar

[13]

Mozilla Metrics. Firefox usage: https://metrics.mozilla.com/.

Google Scholar

[14]

Robin Milner. Communication and Concurrency. Prentice Hall, 1995.

Digital Library

Google Scholar

[15]

Magnus O. Myreen. Verified just-in-time compiler on x86. In POPL '10, pages 107--118. ACM, 2010.

Digital Library

Google Scholar

[16]

Frank Pfenning. A proof of the Church-Rosser theorem and its rep- resentation in a logical framework. Journal of Automated Reasoning, 1993.

Google Scholar

[17]

Kristian Støvring and Soren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In POPL '07, pages 161--172. ACM, 2007.

Digital Library

Google Scholar

[18]

Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. In POPL '04, pages 161--172. ACM, 2004.

Digital Library

Google Scholar

[19]

Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. In POPL '05, pages 63--74. ACM, 2005.

Digital Library

Google Scholar

[20]

Mitchell Wand. Compiler correctness for parallel languages. In FPCA, pages 120--134, 1995.

Digital Library

Google Scholar

[21]

Mitchell Wand and William D. Clinger. Set constraints for destructive array update optimization. Journal of Functional Programmng, 11(3):319--346, 2001.

Digital Library

Google Scholar

[22]

Mitchell Wand and Igor Siveroni. Constraint systems for useless variable elimination. In POPL '99, pages 291--302. ACM, 1999.

Digital Library

Google Scholar

Cited By

View all

Pelenitsyn ABelyakova JChung BTate RVitek J(2021)Type stability in Julia: avoiding performance pathologies in JIT compilationProceedings of the ACM on Programming Languages10.1145/34855275:OOPSLA(1-26)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485527
Barrière ABlazy SFlückiger OPichardie DVitek J(2021)Formally verified speculation and deoptimization in a JIT compilerProceedings of the ACM on Programming Languages10.1145/34343275:POPL(1-26)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434327
Brown FRenner JNötzli ALerner SShacham HStefan DDonaldson ATorlak E(2020)Towards a verified range analysis for JavaScript JITsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385968(135-150)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385968
Show More Cited By

Index Terms

The essence of compiling with traces
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Correctness of speculative optimizations with dynamic deoptimization

High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set ...
Trace-based compilation in execution environments without interpreters
PPPJ '10: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java

Trace-based compilation is a technique used in managed language runtimes to detect and compile frequently executed program paths. The goal is to reduce compilation time and improve code quality by only considering "hot" parts of methods for compilation. ...
The essence of compiling with traces
POPL '11

The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox's JavaScript engine. A trace-based JIT compiler leverages run-time profiling to ...

Reviews

Reviewer: William M. Waite

A widely quoted rule of thumb says that a program spends 90 percent of its time in ten percent of its code. Can we record sequences of instructions (traces) that the program executes very frequently, optimize them in isolation, and make the program run a lot faster__?__ Guo and Palsberg provide us with the theory to safely do just that. Using notation developed in the late 1980s to describe concurrent processes, they characterize the process of recording traces, and prove that some optimizations are sound and others are not. Their goal is to provide a framework for reasoning about the soundness of trace optimizations, not to validate any particular optimization strategy. The treatment is formal, although it includes good examples to develop the reader's intuition. Since I had no experience with the proof techniques used, I found the paper heavy going. The authors provide an excellent reference list, with pointers to sources that are necessary for understanding the notation and terminology. After some concentrated study, I could follow their development, but I'm not convinced that I would be able to reason about a different optimization without more background. 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

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2011

652 pages

ISBN:9781450304900

DOI:10.1145/1926385

General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

ACM SIGPLAN Notices Volume 46, Issue 1
POPL '11
January 2011
624 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1925844
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]

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '11

Sponsor:

SIGPLAN

POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 26 - 28, 2011

Texas, Austin, 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

28
Total Citations
View Citations
616
Total Downloads

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

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pelenitsyn ABelyakova JChung BTate RVitek J(2021)Type stability in Julia: avoiding performance pathologies in JIT compilationProceedings of the ACM on Programming Languages10.1145/34855275:OOPSLA(1-26)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485527
Barrière ABlazy SFlückiger OPichardie DVitek J(2021)Formally verified speculation and deoptimization in a JIT compilerProceedings of the ACM on Programming Languages10.1145/34343275:POPL(1-26)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434327
Brown FRenner JNötzli ALerner SShacham HStefan DDonaldson ATorlak E(2020)Towards a verified range analysis for JavaScript JITsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385968(135-150)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385968
Dumitrescu DStoenescu RPopovici MNegreanu LRaiciu CLorch JYu M(2019)Dataplane equivalence and its applicationsProceedings of the 16th USENIX Conference on Networked Systems Design and Implementation10.5555/3323234.3323290(683-697)Online publication date: 26-Feb-2019
https://dl.acm.org/doi/10.5555/3323234.3323290
Lee WSlaughter EBauer MTreichler SWarszawski TGarland MAiken A(2018)Dynamic tracingProceedings of the International Conference for High Performance Computing, Networking, Storage, and Analysis10.5555/3291656.3291702(1-13)Online publication date: 11-Nov-2018
https://dl.acm.org/doi/10.5555/3291656.3291702
D'Elia DDemetrescu C(2018)On-stack replacement, distilledACM SIGPLAN Notices10.1145/3296979.319239653:4(166-180)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192396
D'Elia DDemetrescu CFoster JGrossman D(2018)On-stack replacement, distilledProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192396(166-180)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192396
Lee WSlaughter EBauer MTreichler SWarszawski TGarland MAiken A(2018)Dynamic tracingProceedings of the International Conference for High Performance Computing, Networking, Storage, and Analysis10.1109/SC.2018.00037(1-13)Online publication date: 11-Nov-2018
https://dl.acm.org/doi/10.1109/SC.2018.00037
Flückiger OScherer GYee MGoel AAhmed AVitek J(2017)Correctness of speculative optimizations with dynamic deoptimizationProceedings of the ACM on Programming Languages10.1145/31581372:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158137
Dissegna SLogozzo FRanzato F(2016)An Abstract Interpretation-Based Model of Tracing Just-in-Time CompilationACM Transactions on Programming Languages and Systems10.1145/285313138:2(1-50)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2853131
Show More Cited By

View Options

Get Access

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

Correctness of speculative optimizations with dynamic deoptimization

Trace-based compilation in execution environments without interpreters