Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
Hazard pointers (HP) is one of the earliest manual memory reclamation algorithms for concurrent data structures. It is widely used for its robustness: memory overhead is bounded (e.g., by the number of threads). To access a node, threads first announce the protection of each to-be-accessed node, which prevents its reclamation. After announcement, they validate the node's reachability from the root to ensure that no threads have missed the announcement and reclaimed it. Traversal-based data structures typically takes a marking-based validation strategy. This strategy uses a node's mark to indicate whether the node is to be detached. Unmarked nodes are considered safe to traverse as both the node and its successors are still reachable, while marked nodes are considered unsafe. However, this strategy is inapplicable to the efficient optimistic traversal strategy that skips over marked nodes.
We propose a new validation strategy for HP that supports lock-free data structures with optimistic traversal, such as lists, trees, and skip lists. The key idea is to exploit the immutability of marked nodes, and validate their reachability at once by checking the reachability of the most recent unmarked node. To ensure correctness, we prove the safety of Harris's list protected with the new strategy in Rocq using the Iris separation logic framework. We show that the new strategy's performance is competitive with state-of-the-art reclamation algorithms when applied to data structures with optimistic traversal, while remaining simple and robust.
Fri 20 JunDisplayed time zone: Seoul change
10:30 - 12:10 | |||
10:30 20mTalk | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation LogicDistinguished Paper PLDI Research Papers Jaehwang Jung Rebellions Inc, Sunho Park KAIST, Janggun Lee KAIST, Jeho Yeon KAIST, Jeehoon Kang KAIST DOI | ||
10:50 20mTalk | Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals PLDI Research Papers DOI | ||
11:10 20mTalk | Iso: Request-Private Garbage Collection PLDI Research Papers Tianle Qiu Australian National University, Stephen M. Blackburn Google; Australian National University DOI | ||
11:30 20mTalk | CRGC: Fault-Recovering Actor Garbage Collection in Pekko PLDI Research Papers Dan Plyukhin University of Southern Denmark, Gul Agha University of Illinois at Urbana-Champaign, Fabrizio Montesi University of Southern Denmark DOI | ||
11:50 20mTalk | RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures PLDI Research Papers DOI |