The essence of compiling with traces

The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox’s JavaScript engine. A trace-based JIT compiler leverages run-time profiling to optimize frequently-executed paths while enabling the optimized code to “bail out” to the original code when the path has been invalidated. This optimization strategy differs from those of other JIT compilers and opens the question of which trace optimizations are sound. In this paper we present a framework for reasoning about the soundness of trace optimizations, and we show that some traditional optimization techniques are sound when used in a trace compiler while others are unsound. The converse is also true: some trace optimizations are sound when used in a traditional compiler while others are unsound. So, traditional and trace optimizations form incomparable sets. Our setting is an imperative calculus for which tracing is exp...

• Type: Journal
• Year: 2011
• Where: POPL
• Authors: Shu-yu Guo, Jens Palsberg
• Keywords: Compiler Correctness, Correctness Proofs, Jit Compilers, POPL 2011, Programming Languages