Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
summary
Proposes modular, machine-checked specs for hazard pointers and RCU and proves realistic reclamation implementations in Coq, mechanized in Iris. Claims compositional verification, general applicability, and low proof overhead; verifies Harris’s list, Harris-Michael list, Chase-Lev deque and RDCSS with reclamation (first proofs with manual reclamation). Introduces managed/protected pointer predicates and a block invariant for mutation, formalizes marking/validation protocol, and ships artifacts and Coq proofs for replication. modular hazard pointer and RCU specs Coq mechanization in Iris verified Harris’s list and Chase-Lev deque
AI-written summary · about
chapters (12)
- 0:00Modular verification intro
- 0:22Memory reclamation problem
- 1:45Goal of verifying libraries
- 2:50Hazard Pointers in lists
- 6:30Naive approach recap
- 8:18Separate permissions for nodes
- 10:09Block invariants for generality
- 11:14List verification with invariants
- 12:18RCU reclamation verification
- 13:20Formalization in Iris
- 14:01Summary and future work
- 14:24Q&A
related talks
15mModular Verification of Op-Based CRDTs in Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
28mReasoning about Distributed Reconfigurable Systems
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mModal Abstractions for Virtualizing Memory Addresses
15mModular Reasoning about Global Variables and Their Initialization
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
21mMechanised Hypersafety Proofs about Structured Data