Verifying a compiler through equational means
summary
Library code models LLVM-like IR as coinductive Interaction Trees and a companion Vellvm semantics on GitHub, represents each syntax node as an ITree with events for locals, memory, calls, undefined/poison and uses a q-value oracle for nondeterminism. Handlers interpret events into state; an extracted OCaml interpreter runs programs. Proofs use equational refinement laws to show per-pass correctness compositionally; approach validates on a realistic sequential LLVM subset and yields executable semantics plus mechanized refinement proofs.
AI-written summary · about
chapters (26)
- 0:00Intro
- 1:16Verifying a compiler
- 2:51Verified Compilation
- 5:00CompCert [Leroy et al.]
- 7:34A time-tested methodology, but...
- 10:41While you are stuck with me...
- 14:35Interaction trees
- 22:27A general recipe
- 23:56LLVM Compiler Infrastructure
- 24:24LLVM IR Semantics
- 26:42Effects: a mixed bag
- 29:45Undef, Undefined Behavior
- 33:51Compositional representation
- 40:41Implementation of effects
- 44:19You can play with it yourself!
- 47:09Equational theory (excerpt)
- 49:57A refinement of VIR programs
- 50:56Compositional reasoning
- 52:13Relaxing the refinement
- 53:38Hence a hierarchy of equivalences
- 54:08Instruction-level reasoning
- 55:06Two main reasoning ingredients
- 55:42SPIRAL HELIX
- 55:55HELIX compilation pipeline
- 56:33Compiler correctness proof
- 58:56What is next?
related talks
01h 06mVerifying a compiler through equational means
23mVellvm: Formalizing the Informal
53mFrom Within: Compiler Testing and Validation via Compilers
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
29mTowards Formally Verified Just-In-Time Compilation
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
29mMechanized monadic equational reasoning for ML references