Formally verified speculation and deoptimization in a JIT compiler

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Formally verified speculation and deoptimization in a JIT compiler

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Formally verified speculation and deoptimization in a JIT compiler

Popis výsledku anglicky

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.

Druh

J_ost - Ostatní články v recenzovaných periodicích

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF15_003%2F0000421" target="_blank" >EF15_003/0000421: Big Code: Škálovatelná analýza rozsáhlých bází programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Proceedings of the ACM on Programming Languages (PACMPL)

ISSN

2475-1421

e-ISSN

—

Svazek periodika

5

Číslo periodika v rámci svazku

POPL

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

26

Strana od-do

1-26

Kód UT WoS článku

000679806100046

EID výsledku v databázi Scopus

2-s2.0-85099022479