Formally verified speculation and deoptimization in a JIT compiler
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F21%3A00347257" target="_blank" >RIV/68407700:21240/21:00347257 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1145/3434327" target="_blank" >https://doi.org/10.1145/3434327</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3434327" target="_blank" >10.1145/3434327</a>
Alternative languages
Result language
angličtina
Original language name
Formally verified speculation and deoptimization in a JIT compiler
Original language description
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. This form of software speculation requires support for deoptimization when some of the assumptions fail to hold. This paper presents a model just-in-time compiler with an intermediate representation that explicits the synchronization points used for deoptimization and the assumptions made by the compiler's speculation. We also present several common compiler optimizations that can leverage speculation to generate improved code. The optimizations are proved correct with the help of a proof assistant. While our work stops short of proving native code generation, we demonstrate how one could use the verified optimization to obtain significant speed ups in an end-to-end setting. 2021 Owner/Author.
Czech name
—
Czech description
—
Classification
Type
J<sub>ost</sub> - Miscellaneous article in a specialist periodical
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF15_003%2F0000421" target="_blank" >EF15_003/0000421: Big Code: Scalable Analysis of Massive Code Bases</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Proceedings of the ACM on Programming Languages (PACMPL)
ISSN
2475-1421
e-ISSN
—
Volume of the periodical
5
Issue of the periodical within the volume
POPL
Country of publishing house
US - UNITED STATES
Number of pages
26
Pages from-to
1-26
UT code for WoS article
000679806100046
EID of the result in the Scopus database
2-s2.0-85099022479