A Mechanically Verified Garbage Collector for OCaml
summary
Verified stop‑the‑world mark‑and‑sweep GC implemented from scratch, mechanized in F with its low‑level subset Low and extracted to C via KaRaMel, then linked into OCaml 4.14.1. Proofs relate mark to a DFS on an abstract object graph (handles infix/internal pointers, closure field starts), sweep coalesces free blocks, and a preserved reachable subgraph guarantee gives safety; liveness holds except where merging complicates reasoning. Benchmarks versus stock OCaml GC and Boehm show stable runs and pragmatic performance; mark‑stack overflow is avoided by assuming stack >= heap.
AI-written summary · about
chapters (8)
- 0:00Verified GC in OCaml
- 3:12F* proof-oriented approach
- 7:07Graph reachability in F*
- 13:46Mark phase correctness
- 18:24Sweep phase with coalescing
- 20:30Verification effort
- 21:55Performance benchmarks
- 23:30Q&A
related talks
50mAn insight into Go Garbage Collection
14mPathological Cases for a Class of Reachability-Based Garbage Collectors
23mTargeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
34mIt's dangerous to GC alone. Take this!
28mA Write Barrier Validating GC for Ruby
21mGarbage Collection for Higher Inductive Types
16mSound Garbage Collection for C using Pointer Provenance
26mAn Invitation to OCaml