Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
summary
First formal verification of a general-purpose RCU under relaxed memory consistency, proving a modular spec that supports modular specification, switchable critical sections, concurrent writers and handling per-node incoming-link histories instead of a total link order. Mechanized proofs live in iRC11 (Iris, Rocq), verify an epoch-based RCU implementation and Peterson’s mutex via a new SC-fence RAW synchronization rule, and reproduce fixes for the real-world Crosswind queue bug; artifacts and reproducible proofs are available.
AI-written summary · about
chapters (10)
- 0:00RCU verification under relaxed memory
- 1:50Memory reclamation in lock-free concurrency
- 4:00Pointed-by assertions for safe reclamation
- 7:08Pointed-by assertions in relaxed memory
- 10:22Verifying RCU data structures in RMC
- 11:26Read-after-write synchronization
- 13:32New proof rule for SC fence
- 15:45Verifying RCU with sense logic
- 16:26Conclusion and mechanized proofs
- 16:46Q&A
related talks
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
28mRevisit Multi-Reader Synchronizations for Scalable Applications
01h 08mRead, Copy, Update, then what? RCU for non-kernel programmers
55m“A lock-free concurrency toolkit for deferred reclamation and optimistic speculation"
17mExploring a real life RCU use case for Rust
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz