一句话：提出以对象修改序（OMO）为核心的证明配方，在 Coq 的 iRC11 分离逻辑中首次验证弱内存下多个并发对象的线性一致性。
线性一致性是并发对象正确性的事实标准，要求对象的所有操作表现得如同原子执行。近年来针对松弛内存一致性（RMC）的线性一致性规格不断增强，但由于乱序执行需要事件重排、选择性同步需要追踪视图传递，可扩展的证明方法始终缺失。本文在基于 Iris 的 iRC11 并发分离逻辑（Coq）中，为 Dang 等人提出的线性化历史规格给出了一套证明配方。其核心概念是对象修改序（OMO），它将 C11 内存模型中的修改序推广到对象局部场景，从而最小化事件重排所需证明的条件；OMO 还提供了新的 commit-with 关系，连接下层与上层库的线性化点，以支持在已有库之上构建的并发库的证明复用。作者在 Coq 中机械化该配方，首次验证了 Michael–Scott 队列、elimination stack 与 Folly 的 MPMC 队列在 RMC 下的线性一致性，并验证了自旋锁与原子引用计数比此前工作更强的规格。
Linearizability is the de facto standard for correctness of concurrent objects–it essentially says that all the object’s operations behave as if they were atomic. There have been a number of recent advances in developing increasingly strong linearizability specifications for relaxed memory consistency (RMC), but scalable proof methods for these specifications do not exist due to the challenges arising from out-of-order executions (requiring event reordering) and selected synchronization (requiring tracking of view transfers). We propose a proof recipe for the linearizable history specifications by Dang et al . in the Iris-based iRC11 concurrent separation logic in Coq. Key to our proof recipe is the notion of object modification order (OMO) , which generalizes the modification order of the C11 memory model to an object-local setting. Using OMO we minimize the conditions that need to be proved for event reordering. To enable proof reuse for concurrent libraries that are built on top of others, OMO provides the novel notion of a commit-with relation that connects the linearization points of the lower and upper libraries. Using our recipe, we verify the linearizability of the Michael–Scott queue, the elimination stack, and Folly’s MPMC queue in RMC for the first time; and verify stronger specifications of a spinlock and atomic reference counting in RMC than prior work.
@article{ParkKMJLKK24,
title = {A Proof Recipe for Linearizability in Relaxed Memory Separation Logic},
author = {Sunho Park and Jaewoo Kim and Ike Mulder and Jaehwang Jung and Janggun Lee and Robbert Krebbers and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656384}
}