A Formal Foundation for Trace-based JIT Compilers

Trace-based JIT compilers identify frequently executed pro-gram paths at run-time and subsequently record, compile and optimize their execution. In order to improve the per-formance of the generated machine instructions, JIT com-pilers heavily rely on dynamic analysis of the code. Existing work treats the components of a JIT compiler as a monolithic whole, tied to particular execution semantics. We propose a formal framework that facilitates the design and implemen-tation of a tracing JIT compiler and its accompanying dy-namic analyses by decoupling the tracing, optimization, and interpretation processes. This results in a framework that is more configurable and extensible than existing formal trac-ing models. We formalize the tracer and interpreter as two abstract state machines that communicate through a mini-mal, well-defined interface. Developing a tracing JIT com-piler becomes possible for arbitrary interpreters that imple-ment this interface. The abstract machines also provide the necessary hooks to plug in custom analyses and optimiza-tions. Categories and Subject Descriptors D.3.1 [Formal Defini-tions and Theory]: semantics; D.3.4 [Processors]: compil-ers, optimizatio