PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
Fri 20 Jun 2025 10:50 - 11:10 at Cosmos, Violet & Tulip - Memory Management Chair(s): Erez Petrank

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 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Memory ManagementPLDI Research Papers at Cosmos, Violet & Tulip
Chair(s): Erez Petrank Technion
10:30
20m
Talk
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
20m
Talk
Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
PLDI Research Papers
DOI
11:10
20m
Talk
Iso: Request-Private Garbage Collection
PLDI Research Papers
Tianle Qiu Australian National University, Stephen M. Blackburn Google; Australian National University
DOI
11:30
20m
Talk
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
20m
Talk
RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures
PLDI Research Papers
Md Amit Hasan Arovi Pennsylvania State University, Ruslan Nikolaev Pennsylvania State University
DOI