An Abstract Interpretation-based Model of Tracing Just-In-Time Compilation

TL;DR

This paper presents a formal abstract interpretation-based model for tracing JIT compilation, providing a rigorous framework for correctness and generality in dynamic program optimization techniques.

Contribution

It introduces a generic, formal model for tracing JIT compilation using abstract interpretation, and proves correctness of specific optimizations like type specialization and constant folding.

Findings

Framework is more general than previous models.

Proves correctness of dynamic type specialization.

Validates constant variable folding correctness.

Abstract

Tracing just-in-time compilation is a popular compilation technique for the efficient implementation of dynamic languages, which is commonly used for JavaScript, Python and PHP. We provide a formal model of tracing JIT compilation of programs using abstract interpretation. Hot path detection corresponds to an abstraction of the trace semantics of the program. The optimization phase corresponds to a transform of the original program that preserves its trace semantics up to an observation modeled by some abstraction. We provide a generic framework to express dynamic optimizations and prove them correct. We instantiate it to prove the correctness of dynamic type specialization and constant variable folding. We show that our framework is more general than the model of tracing compilation introduced by Guo and Palsberg [2011] based on operational bisimulations.