AI 中文总结
研究并发数据结构线性一致性中逻辑原子性规范与线性一致性的关系，证明Iris分离逻辑框架下能为线性一致数据结构导出逻辑原子性规范，将多种证明技术嵌入Iris并应用于多个队列实现，还建立相关联系并机械化结果。
AI 中文摘要
线性一致性是并发数据结构的标准正确性条件，它保证操作行为如同在调用和返回点之间的某个原子时刻生效。此前工作提出用逻辑原子性规范代替线性一致性规范，在逻辑推理规则中内化操作的原子性，认为其在逻辑内更易组合。在Iris分离逻辑框架中，某种形式的逻辑原子性规范蕴含数据结构的线性一致性，但反之是否成立是开放问题。本文肯定地解决了该问题，证明了Iris的完备性定理，能为任何线性一致的数据结构导出逻辑原子性规范。还将多种线性一致性证明技术嵌入Iris，应用于Herlihy-Wing队列、Baskets队列和Folly MPMC队列实现，并建立了逻辑原子性与Iris中细化编码的联系，所有结果都在Rocq Prover中机械化。
英文摘要
Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their call and return points. Despite the central role linearizability plays, prior work has argued for instead using a style of specification that internalizes the atomicity of operations in terms of the logic's reasoning rules, known as logical atomicity. These logically atomic specifications are intended to be easier to compose inside of the logic than linearizability. Prior work has shown that in the Iris separation logic framework, a certain form of logically atomic specifications implies that a data structure is linearizable. However, the converse remained an open question: for every linearizable data structure, is it always possible to derive a corresponding logically atomic specification? This paper resolves this question in the affirmative. We prove a completeness theorem for Iris that derives a logically atomic specification for any linearizable data structure. As a consequence, we are able to embed a variety of linearizability proof techniques into Iris and use them to derive logically atomic specifications. We apply this to three linearizability proof methods: aspect-oriented linearizability proofs, forward simulations with commit points, and meta-configuration tracking. Using these embeddings, we derive logically atomic specifications for the Herlihy-Wing queue and the Baskets Queue. We furthermore establish a connection between logical atomicity and an encoding of refinement in Iris that has been used in prior logical relations models. This result allows us to transport logically atomic specifications across refinements, which we apply to the Folly MPMC queue implementation. All of the results in this paper have been mechanized in the Rocq Prover.
