Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
summary
First mechanized verification of a lock-free linked list, skiplist, and skiplist-based priority queue against relaxed memory consistency, using the iRC11 relaxed memory separation logic built on Iris in Coq (Rocq); all proofs are mechanized and artifacts are available and evaluated. Key ideas are per-key linearizable history to permit independent per-key orders and a shadowed-by relation to rule out thread-dependent stale-edge reachability; the verification succeeds on all case studies.
AI-written summary · about
chapters (8)
- 0:00Verifying lock-free traversals
- 1:26Relaxed memory challenges
- 3:12Relaxed memory semantics
- 5:19Per-key linearization spec
- 9:15Thread-dependent reachability
- 13:07Shadow violation in verification
- 14:09Conclusion and future work
- 14:30Q&A
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
16mVerified Lock-Free Session Channels with Linking
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
21mCSL and relaxed memory
26mHigher-Order Leak and Deadlock Free Locks