一句话：在并发分离逻辑中为 hazard pointer 和 RCU 设计模块化抽象谓词，并首次形式验证带内存回收的多个并发数据结构。
并发数据结构的形式验证常忽略内存回收，而回收与并发访问之间的同步若出错会导致 use-after-free 和 ABA 问题。hazard pointer、RCU 等半自动安全回收方案虽以模块化接口封装手动内存管理复杂度，但这一模块性尚未延续到形式验证。本文在并发分离逻辑中提出 hazard pointer 与 RCU 的模块化规约，设计抽象谓词分别刻画节点保护验证和乐观遍历已退休节点的语义，并在 Iris 框架中用 Coq 机器化验证其现实实现。工作从组合式验证、通用适用性和易集成三方面展示规约的模块化能力，并首次形式验证了带回收的 Harris 表、Harris-Michael 表、Chase-Lev deque 与 RDCSS。
Formal verification is an effective method to address the challenge of designing correct and efficient concurrent data structures. But verification efforts often ignore memory reclamation , which involves nontrivial synchronization between concurrent accesses and reclamation. When incorrectly implemented, it may lead to critical safety errors such as use-after-free and the ABA problem. Semi-automatic safe memory reclamation schemes such as hazard pointers and RCU encapsulate the complexity of manual memory management in modular interfaces. However, this modularity has not been carried over to formal verification. We propose modular specifications of hazard pointers and RCU, and formally verify realistic implementations of them in concurrent separation logic. Specifically, we design abstract predicates for hazard pointers that capture the meaning of validating the protection of nodes, and those for RCU that support optimistic traversal to possibly retired nodes. We demonstrate that the specifications indeed facilitate modular verification in three criteria: compositional verification, general applicability, and easy integration. In doing so, we present the first formal verification of Harris’s list, the Harris-Michael list, the Chase-Lev deque, and RDCSS with reclamation. We report the Coq mechanization of all our results in the Iris separation logic framework.
@article{paperbot1827,
title = {Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic},
author = {Jaehwang Jung and Janggun Lee and Jaemin Choi and Jaewoo Kim and Sunho Park and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622827}
}