Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr
summary
First formal specification and machine-checked proof of Meta Folly’s fine‑grained MPMC queue: an ML‑style implementation is shown to be a contextual refinement of a simple coarse‑grained, lock‑based queue (hence linearizable). Verification is modular across three modules (turn sequencer, single‑element queue, MPMC), done in Coq mechanization using ReLoC + Iris, and requires a novel extension to ReLoC to handle an external linearization point that is extracted, moved into an invariant, and recombined.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 2:55Design
- 8:10Invariant
- 14:45Questions
- 15:15External vs Helping
- 17:55Logically Automated Triple
- 19:20Question
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
15mCQS: A Formally-Verified Framework for Fair and Abortable Synchronization
19mEfficient Linearizability Monitoring
19mScenario-based Proofs for Concurrent Objects
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz