Proving Highly-Concurrent Traversals Correct
summary
Paper proves that optimistic lock-free traversals are correct by reducing concurrent traversal correctness to sequential reasoning plus two concrete conditions: single-step compatibility (if p is reachable then its child read x is reachable) and the forepassed condition (once a write makes a node unreachable that node becomes immutable or only points to already-reachable nodes). Proofs handle rotations implemented by node-copying, logical and physical delete bits, and discharge on real structures: lazy lists, logical-ordering and contention-friendly trees, and Citrus, making linearizability proofs much simpler.
AI-written summary · about
chapters (5)
related talks
14mLeveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
14mVerifying Concurrent Multicopy Search Structures
24mA Concurrent Program Logic with a Future and History
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
54mReasoning about Progress of Concurrent Objects
20mVisibility Reasoning for Concurrent Snapshot Algorithms
25mThe Path to Durable Linearizability
27mC4: verified transactional objects