Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 16:40 - 16:50 at POPL-A - Compilers & Optimization

Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time in order to specialize that code to the common case and avoid unnecessary overheads. 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. 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 speed up in an end-to-end setting.

Wed 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Compilers & OptimizationPOPL at POPL-A
16:00
10m
Talk
Fully Abstract from Static to Gradual
POPL
Koen JacobsKU Leuven, Amin TimanyAarhus University, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
16:10
10m
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen RouvoetDelft University of Technology, Robbert KrebbersRadboud University Nijmegen, Eelco VisserDelft University of Technology
Link to publication DOI Pre-print
16:20
10m
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha HietalaUniversity of Maryland, Robert RandUniversity of Chicago, Shih-Han HungUniversity of Maryland, USA, Xiaodi WuUniversity of Maryland, USA, Michael HicksUniversity of Maryland at College Park
Link to publication DOI
16:30
10m
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël CourantINRIA, Xavier LeroyCollège de France
Link to publication DOI
16:40
10m
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes, IRISA, Olivier FlückigerNortheastern University, David PichardieUniv Rennes, ENS Rennes, IRISA, Jan VitekNortheastern University / Czech Technical University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL