Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
summary
Presents a new hazard-pointer validation that exploits the immutability of marked nodes to validate reachability by checking the most recent unmarked predecessor, enabling true optimistic traversal without restarting. Proves safety for Harris's list in Rocq using the Iris separation logic framework, provides reusable artifacts, and shows performance gains over pessimistic validation up to 24% for lists and 61% for trees while remaining simple, lock-free, and competitive with state-of-the-art reclamation.
AI-written summary · about
chapters (11)
- 0:00Hazard pointers and immutability
- 1:05Reclamation methods like RCU
- 2:09Preventing use-after-free errors
- 3:35Node detachment and validation
- 5:03Problem with standard validation
- 6:51Performance versus robustness
- 7:33Immutability in traversals
- 8:38ValImmut validation strategy
- 10:04Experimental results and gains
- 10:51Conclusion and future work
- 11:17Q&A
related talks
12mProving Highly-Concurrent Traversals Correct
58m“The Landscape and Exciting New Future of Safe Reclamation for High Performance”
51mA (Simple) Hazard Pointer Update
55m“A lock-free concurrency toolkit for deferred reclamation and optimistic speculation"
25mThe Path to Durable Linearizability
23mVerifying Observational Robustness Against a C11-style Memory Model
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
14mVerifying Concurrent Multicopy Search Structures