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. This form of software speculation requires supp...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2021-01, Vol.5 (POPL), p.1-26
Main Authors: Barrière, Aurèle, Blazy, Sandrine, Flückiger, Olivier, Pichardie, David, Vitek, Jan
Format: Article
Language:English
Subjects:
Computer Science
Programming Languages
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2475-1421
2475-1421
DOI:10.1145/3434327