一句话：首次在松弛内存模型下形式化验证具备模块化规约、可切换临界区与并发写者支持的通用 RCU。
RCU 是并发数据结构中用于延迟内存回收的关键同步机制，但正确实现和使用因并发复杂性而困难。已有验证工作要么假设顺序一致内存模型，要么缺少通用 RCU 库的三大特性：模块化规约、可切换临界区和并发写者支持。本文给出首个在真实松弛内存一致性模型下对通用 RCU 的形式化验证。为涵盖松弛行为，作者扩展现有 SC 规约以显式同步；为支持需要写后读同步的可切换临界区，提出 RAW 同步 SC fence 的推理原则，并据此首次在松弛内存下验证 Peterson 互斥锁；为处理并发写者的部分有序写入，采用逐节点入链接历史不变量。证明在基于 Iris 的 iRC11 松弛内存分离逻辑中机械化，使用 Rocq。
Read-Copy-Update (RCU) is a critical synchronization mechanism for concurrent data structures, enabling efficient deferred memory reclamation. However, implementing and using RCU correctly is challenging due to its inherent concurrency complexities. While previous work verified RCU, they either relied on unrealistic assumptions of sequentially consistent (SC) memory model or lacked three key features of general-purpose RCU libraries: modular specification, switchable critical sections, and concurrent writer support. We present the first formal verification of a general-purpose RCU in realistic relaxed memory consistency (RMC), addressing the challenges posed by these features. To achieve modular specification that encompasses relaxed behaviors, we extend existing SC specifications to account for explicit synchronization. To support switchable critical sections, which require read-after-write (RAW) synchronization, we introduce a reasoning principle for RAW-synchronizing SC fences . Using this principle, we also present the first formal verification of Peterson's mutex in RMC. To support concurrent writers performing partially ordered writes, we avoid assuming a total order of links and instead formulate invariants based on per-node incoming link histories. Our proofs are mechanized in the iRC11 relaxed memory separation logic, built upon Iris, in Rocq.
@article{paperbot3147,
title = {Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic},
author = {Jaehwang Jung and Sunho Park and Janggun Lee and Jeho Yeon and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729246}
}