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

research-article

Open access

Correctness of speculative optimizations with dynamic deoptimization

Authors:

Olivier Flückiger,

Gabriel Scherer,

Jan VitekAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 49, Pages 1 - 28

https://doi.org/10.1145/3158137

Published: 27 December 2017 Publication History

Abstract

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 of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that are no longer valid. The implementation must then deoptimize the program on-the-fly; this entails finding semantically equivalent code that does not rely on invalid assumptions, translating program state to that expected by the target code, and transferring control. This paper looks at the interaction between optimization and deoptimization, and shows that reasoning about speculation is surprisingly easy when assumptions are made explicit in the program representation. This insight is demonstrated on a compiler intermediate representation, named sourir, modeled after the high-level representation for a dynamic language. Traditional compiler optimizations such as constant folding, unreachable code elimination, and function inlining are shown to be correct in the presence of assumptions. Furthermore, the paper establishes the correctness of compiler transformations specific to deoptimization: namely unrestricted deoptimization, predicate hoisting, and assume composition.

Supplementary Material

WEBM File (speculativeoptimization.webm)

Download
92.29 MB

References

[1]

Vasanth Bala, Evelyn Duesterwald, and Sanjeev Banerjia. 2000. Dynamo: A Transparent Dynamic Optimization System. In Programming Language Design and Implementation (PLDI).

Digital Library

[2]

Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter. 2010. SP UR: A Trace-based JIT Compiler for CIL. In Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA).

Digital Library

[3]

Clément Béra, Eliot Miranda, Marcus Denker, and Stéphane Ducasse. 2016. Practical validation of bytecode to bytecode JIT compiler dynamic deoptimization. Journal of Object Technology (JOT) 15, 2 (2016).

[4]

Project Chromium. 2017. V8 JavaScript Engine. https://chromium.googlesource.com/v8/v8.git .

[5]

Daniele Cono D’Elia and Camil Demetrescu. 2016. Flexible on-stack replacement in LLVM. In Code Generation and Optimization (CGO).

Digital Library

[6]

Stefano Dissegna, Francesco Logozzo, and Francesco Ranzato. 2014. Tracing Compilation by Abstract Interpretation. In Principles of Programming Languages (POPL).

Digital Library

[7]

Gilles Duboscq, Thomas Würthinger, and Hanspeter Mössenböck. 2014. Speculation without regret: reducing deoptimization meta-data in the Graal compiler. In Principles and Practices of Programming on the Java Platform (PPPJ).

[8]

Gilles Duboscq, Thomas Würthinger, Lukas Stadler, Christian Wimmer, Doug Simon, and Hanspeter Mössenböck. 2013. An Intermediate Representation for Speculative Optimizations in a Dynamic Compiler. In Virtual Machines and Intermediate Languages (VMIL).

Digital Library

[9]

Stephen J. Fink and Feng Qian. 2003. Design, Implementation and Evaluation of Adaptive Recompilation with On-stack Replacement. In Code Generation and Optimization (CGO).

[10]

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. 2009. Trace-based Just-in-time Type Specialization for Dynamic Languages. In Programming Language Design and Implementation (PLDI).

Digital Library

[11]

Shu-yu Guo and Jens Palsberg. 2011. The Essence of Compiling with Traces. In Principles of Programming Languages (POPL).

Digital Library

[12]

Urs Hölzle, Craig Chambers, and David Ungar. 1992. Debugging Optimized Code with Dynamic Deoptimization. In Programming Language Design and Implementation (PLDI).

Digital Library

[13]

Kazuaki Ishizaki, Motohiro Kawahito, Toshiaki Yasue, Hideaki Komatsu, and Toshio Nakatani. 2000. A Study of Devirtualization Techniques for a Java Just-In-Time Compiler. In Object-oriented Programming Systems, Language, and Applications (OOPSLA).

Digital Library

[14]

Gary A. Kildall. 1973. A Unified Approach to Global Program Optimization. In Principles of Programming Languages (POPL).

Digital Library

[15]

Xavier Leroy and Sandrine Blazy. 2008. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning 41, 1 (2008).

Digital Library

[16]

Magnus O. Myreen. 2010. Verified Just-in-time Compiler on x86. In Principles of Programming Languages (POPL).

Digital Library

[17]

Rei Odaira and Kei Hiraki. 2005. Sentinel PRE: Hoisting Beyond Exception Dependency with Dynamic Deoptimization. In Code Generation and Optimization (CGO).

Digital Library

[18]

Michael Paleczny, Christopher Vick, and Cliff Click. 2001. The Java Hotspot Server Compiler. In Java Virtual Machine Research and Technology (JVM). http://www.usenix.org/events/jvm01/full_papers/paleczny/paleczny.pdf

[19]

Amr Sabry and Matthias Felleisen. 1992. Reasoning About Programs in Continuation-passing Style. In LISP and Functional Programming (LFP).

Digital Library

[20]

David Schneider and Carl Friedrich Bolz. 2012. The efficient handling of guards in the design of RPython’s tracing JIT. In Workshop on Virtual Machines and Intermediate Languages (VMIL).

Digital Library

[21]

Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2007. Ott: Effective Tool Support for the Working Semanticist. In International Conference on Functional Programming (ICFP).

Digital Library

[22]

Sunil Soman and Chandra Krintz. 2006. Efficient and General On-Stack Replacement for Aggressive Program Specialization. In Software Engineering Research and Practice (SERP).

[23]

Kunshan Wang, Yi Lin, Stephen M. Blackburn, Michael Norrish, and Antony L. Hosking. 2015. Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. In Summit on Advances in Programming Languages (SNAPL), Vol. 32.

[24]

Yudi Zheng, Lubomír Bulej, and Walter Binder. 2017. An Empirical Study on Deoptimization in the Graal Compiler. In European Conference on Object-Oriented Programming (ECOOP).

Cited By

Barrière ABlazy SPichardie D(2023)Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT CompilerProceedings of the ACM on Programming Languages10.1145/35712027:POPL(249-277)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571202
Goharshady AZaher A(2023)Efficient Interprocedural Data-Flow Analysis Using Treedepth and TreewidthVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-24950-1_9(177-202)Online publication date: 17-Jan-2023
https://doi.org/10.1007/978-3-031-24950-1_9
Qin QJiYang JSong FChen TXing XRoychoudhury ACadar CKim M(2022)DeJITLeak: eliminating JIT-induced timing side-channel leaksProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549150(872-884)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549150
Show More Cited By

Index Terms

Correctness of speculative optimizations with dynamic deoptimization
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Just-in-time compilers

Recommendations

Formally verified speculation and deoptimization in a JIT compiler

Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. ...
An approach to compiler correctness
International Conference on Reliable Software

This paper is a preliminary report on an experiment in applying Floyd's method of inductive assertions to the compiler correctness problem. Practical postfix translators are considered, and the semantics of source and object languages are characterized ...
An approach to compiler correctness
Proceedings of the international conference on Reliable software

This paper is a preliminary report on an experiment in applying Floyd's method of inductive assertions to the compiler correctness problem. Practical postfix translators are considered, and the semantics of source and object languages are characterized ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

ONR
European Research Council (ERC)
NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
726
Total Downloads

Downloads (Last 12 months)122
Downloads (Last 6 weeks)15

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Barrière ABlazy SPichardie D(2023)Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT CompilerProceedings of the ACM on Programming Languages10.1145/35712027:POPL(249-277)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571202
Goharshady AZaher A(2023)Efficient Interprocedural Data-Flow Analysis Using Treedepth and TreewidthVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-24950-1_9(177-202)Online publication date: 17-Jan-2023
https://doi.org/10.1007/978-3-031-24950-1_9
Qin QJiYang JSong FChen TXing XRoychoudhury ACadar CKim M(2022)DeJITLeak: eliminating JIT-induced timing side-channel leaksProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549150(872-884)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549150
Flückiger OJečmen JKrynski SVitek JJhala RDillig I(2022)Deoptless: speculation with dispatched on-stack replacement and specialized continuationsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523729(749-761)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523729
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
Polito GTesone PDucasse SFabresse LRogliano TMisse-Chanabier PHernandez Phillips CKuchen HSinger J(2021)Cross-ISA testing of the Pharo VM: lessons learned while porting to ARMv8Proceedings of the 18th ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes10.1145/3475738.3480715(16-25)Online publication date: 29-Sep-2021
https://dl.acm.org/doi/10.1145/3475738.3480715
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
Flückiger OChari GYee MJečmen JHain JVitek J(2020)Contextual dispatch for function specializationProceedings of the ACM on Programming Languages10.1145/34282884:OOPSLA(1-24)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428288
Belyakova JChung BGelinas JNash JTate RVitek J(2020)World age in Julia: optimizing method dispatch in the presence of evalProceedings of the ACM on Programming Languages10.1145/34282754:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428275
Chatterjee KGoharshady AIbsen-Jensen RPavlogiannis A(2020)Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow AnalysisProgramming Languages and Systems10.1007/978-3-030-44914-8_5(112-140)Online publication date: 18-Apr-2020
https://doi.org/10.1007/978-3-030-44914-8_5
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents