一句话：首次在松弛内存一致性下形式验证无锁链表、跳表及跳表优先队列，提出逐键线性化历史规约与 shadowed-by 关系。
松弛内存一致性允许内存访问重排序，给无锁数据结构的遍历验证带来两大挑战：一是规约需灵活捕捉松弛行为又易于理解使用；二是遍历线程可能读到过期边，难以推理边可达性。本文首次对无锁链表、跳表及跳表优先队列进行形式验证，提出逐键线性化历史规约，仅要求每个键上的操作满足尊重因果的全序，而非所有操作的全局全序。为应对验证挑战，引入 shadowed-by 关系形式化过期边概念，从而为每个键建立边及其关联操作的全序，满足强规约。所有证明均在基于 Iris 框架、用 Rocq 实现的 iRC11 松弛内存分离逻辑中机械化。
We report the first formal verification of a lock-free list, skiplist, and a skiplist-based priority queue against a strong specification in relaxed memory consistency (RMC). RMC allows relaxed behaviors in which memory accesses may be reordered with other operations, posing two significant challenges for the verification of lock-free traversals. (1) Specification challenge : formulating a specification that is flexible enough to capture relaxed behaviors, yet simple enough to be easily understood and used. We address this challenge by proposing the per-key linearizable history specification that enforces a total order of operations for each key that respects causality, rather than a total order of all operations. (2) Verification challenge : devising verification techniques for reasoning about the reachability of edges for traversing threads, which can read stale edges due to relaxed behaviors. We address this challenge by introducing the shadowed-by relation that formalizes the notion of outdated edges. This relation enables us to establish a total order of edges and thus their associated operations for each key, required to satisfy the strong specification. All our proofs are mechanized on the iRC11 relaxed memory separation logic, built on the Iris framework in Rocq.
@article{paperbot3086,
title = {Verifying Lock-Free Traversals in Relaxed Memory Separation Logic},
author = {Sunho Park and Jaehwang Jung and Janggun Lee and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729248}
}