Verifying a compiler through equational means
summary
A machine-checked methodology builds a compositional, equational semantics for an LLVM-like IR using Interaction Trees and a formal IR called VIR/Vellvm, turning language effects (memory, locals, calls, undefined behavior) into typed events and handlers. The team extracts executable interpreters to OCaml, proves those interpreters refine the nondeterministic semantic model, and uses equational laws to show local, modular correctness of compiler passes; a realistic subset and a Spiral-to-IR compilation pipeline serve as a validated case study.
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
53mFrom Within: Compiler Testing and Validation via Compilers
23mVellvm: Formalizing the Informal
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
29mTowards Formally Verified Just-In-Time Compilation
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
50mCompCert: a journey through the landscape of mechanized semantics for verified co...