一句话：提出利用标记节点不可变性的 Hazard Pointer 验证策略，支持乐观遍历的无锁结构，并在 Rocq/Iris 中证明其安全性。
Hazard pointer（HP）是并发数据结构中最早的手工内存回收算法之一，其内存开销有界、鲁棒性强：线程在访问节点前先宣告保护，然后验证该节点仍可从根到达，以确认没有其他线程错过宣告而将其回收。对基于遍历的数据结构，常用做法是基于标记（marking）的验证：未标记节点及其后继仍可达因而安全，已标记节点则不安全。但该策略无法用于会跳过已标记节点的乐观遍历。本文提出一种面向乐观遍历无锁结构（链表、树、跳表等）的新型 HP 验证策略，核心思想是利用已标记节点的不可变性，通过只检查最近一个未标记节点的可达性，一次性验证其后所有已标记节点的可达性。作者在 Rocq 中基于 Iris 分离逻辑框架机器化证明了采用该策略保护的 Harris 链表的安全性，并在实验上表明，对具有乐观遍历的数据结构，其性能与当前最先进的回收算法相当，同时保持简单与鲁棒。
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 use 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.
@article{paperbot3108,
title = {Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals},
author = {Janggun Lee and Jeonghyeon Kim and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729247}
}