Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
summary
Prototype JIT is implemented and mechanically verified in Coq, reusing the CompCert backend and its correctness proofs to generate x86 code, and modeling impurity with a free-monadic encoding that exposes a small set of trusted primitives (install code, stack ops). Proofs combine forward and backward simulations to preserve observable behavior plus stack/heap effects. Extraction yields an executable OCaml/C prototype that outperforms pure interpretation (up to 40x faster on simple tests) using custom calling conventions.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:22Formal Verification
- 2:00Formal Verification Just in Time
- 4:40Formally Verified JIT
- 10:23Monadic Encoding
- 15:07Proof
- 18:48Conclusion
related talks
29mTowards Formally Verified Just-In-Time Compilation
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
58mFast Cryptographic Code via Partial Evaluation
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
15mEfficient Compilation of Algebraic Effect Handlers
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...