Towards Formally Verified Just-In-Time Compilation
summary
A Coq-based JIT middle-end prototype implements an RTL-like IR with an assume instruction (from Suya) to encode speculative checks, plus passes for speculation insertion, constant propagation and function inlining; some passes are machine-verified and the whole model is extracted to executable Gallina. Correctness uses per-pass forward simulations composed into a JIT-style backward simulation, and the design proves the profiler need not be verified for overall safety.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 0:23Static Compilation
- 1:23JustInTime Compilation
- 2:47JIT Compilers
- 3:48Speculative Optimization
- 5:03Speculative Optimization Example
- 5:55JIT Execution Example
- 7:21Previous Work
- 8:57Scope of Work
- 10:15Prototype
- 11:29Formal Proof
- 12:31Backward Simulations
- 13:50Semantic State Matching
- 17:36Speculation
- 19:05Inline Engine
- 19:38Modular Verification
- 20:53Conclusion
- 21:57Further Walks
- 23:08Questions
related talks
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
01h 06mVerifying a compiler through equational means
14mCoSSJIT: Combining Static Analysis and Speculation in JIT Compilers- 01h 06mVerifying a compiler through equational means
18mPreservation of Speculative Constant-time by Compilation
18mPreservation of speculative constant-time by compilation