Tracing Compilation by Abstract Interpretation - Logozzo, Francesco (Proceedings of the 41st Symposium on Programming Languages (POPL'14), 2014)
Tracing just-in-time compilation is a very popular compilation schema for the efficient implementation of dynamic languages, which is used in the most efficient implementations of JavaScript, Python, and PHP. It relies on two key ideas. First, it monitors the execution of the program to detect so-called hot paths, i.e., the most frequently executed paths. Then, it uses some store information available at runtime to optimize hot paths. The result is a residual program where the optimized hot paths are guarded by sufficient conditions ensuring the equivalence of the optimized path and the original program. The residual program is constantly mutated during the execution, e.g., to add new optimized paths or to merge existing paths. Tracing compilation is thus fundamentally different than traditional static compilation. Nevertheless, despite the large industrial success of tracing compilation, very little is known about its theoretical foundations. We formalize tracing compilation using abstract interpretation. The monitoring (viz., hot path detection) phase corresponds to an abstraction of the trace semantics that captures the most frequent occurrences of sequences of program points together with an abstraction of their corresponding stores, e.g., a type environment. The optimization (viz., residual program generation) phase corresponds to a transform of the original program preserving its trace semantics up to a given observation as modeled by some abstraction. We provide a generic framework to express dynamic optimizations and to prove them correct. We instantiate it to prove the correctness of dynamic type specialization. We show that our framework is more general than a recent model of tracing compilation introduced by Guo and Palsberg (based on operational bisimulations). In our model we can naturally express hot path reentrance and common optimizations like dead-store elimination, which are either excluded or unsound in Guo and Palsberg’s framework.