Formally Verified Speculation and Deoptimization in a JIT Compiler

on YouTube ↗23m

" summary

A formal model defines a JIT’s middle end, an RTL-like IR and two concrete speculative ops: the anchor instruction which marks safe deoptimization points and the assume instruction which checks hypotheses and triggers deoptimization. Each optimization pass is proved correct with backward simulations, inlining proves correct by synthesizing missing stack frames, and non-determinism from speculation is handled so standard passes like constant propagation reuse forward-to-backward proofs. An OCaml extraction plus an unverified LLVM backend runs examples and shows measurable speedups though native codegen is not verified.

AI-written summary · about

" chapters (23)

1. 0:00Intro
2. 0:15JIT COMPILATION
3. 1:09FORMALLY VERIFIED STATIC COMPILATION
4. 1:55RUNNING A JIT COMPILER
5. 3:32SPECULATIVE OPTIMIZATIONS IN JIT COMPILERS
6. 4:19SPECULATIVE OPTIMIZATIONS - EXAMPLE
7. 5:16EXECUTING A PROGRAM WITH AJIT
8. 6:08DESIGN AND VERIFICATION CHALLENGES
9. 7:10JIT COMPILERS ARE COMPLEX SOFTWARE
10. 8:02MODELING SPECULATION IN COQ
11. 8:49JIT BEHAVIOR
12. 10:04THE TWO SPECULATIVE INSTRUCTIONS OF CORER
13. 11:28INSERTING SPECULATION
14. 13:04ON-STACK REPLACEMENT: SYNTHESIZING STACKFRAMES
15. 14:17PROVING OPTIMIZATIONS CORRECT IN A STATIC COMPILER
16. 15:16INSERTING NEW SPECULATIONS
17. 16:15LOUD SEMANTICS
18. 17:36A MECHANIZED MIDDLE-END OPTIMIZER WITH SPECULATION
19. 18:34NESTED SIMULATIONS FOR DYNAMIC OPTIMIZATIONS
20. 19:30SPECIFYING A CORRECT JIT
21. 20:20EXTRACTING THE JIT TO OCML
22. 21:19RUNNING COREJIT
23. 22:05A MECHANIZED JIT IN COQ

" related talks

• 29mTowards Formally Verified Just-In-Time CompilationAurèle Barrière · CoqPL 2020
• 24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...Aurèle Barrière, Sandrine Blazy, David Pichardie · POPL 2023
• 19mFormally Verifying Optimizations with Block SimulationsLéo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard · OOPSLA 2023
• 18mPreservation of speculative constant-time by compilationGilles Barthe, Benjamin Gregoire, Santiago Arranz Olmos, Lionel Blatter, Vincent Laporte · POPL 2025
• 14mCoSSJIT: Combining Static Analysis and Speculation in JIT CompilersDaryl Maier, Aditya Anand, Vijay Sundaresan, Manas Thakur · OOPSLA 2025
• 18mPreservation of Speculative Constant-time by CompilationGilles Barthe, Benjamin Gregoire, Santiago Arranz Olmos, Lionel Blatter, Vincent Laporte · PriSC 2025 (with POPL 2025)
• 01h 06mVerifying a compiler through equational meansYannick Zakowski · CoqPL 2021
• 25mExorcising Spectres with Secure CompilersMarco Patrignani · PriSC 2020