We propose an approach for modular verification of programs that use relaxed-consistency atomic memory access primitives and fences. The approach is sufficient for verifying the core of Rust's Atomic Reference Counting (ARC) algorithm. We first argue its soundness, when combined with a simple static analysis and admitting an open sub-problem, with respect to the C20 memory consistency model. We then argue its soundness, even in the absence of any static analysis and without any assumptions, with respect to YC20, a minor strengthening of XC20, itself a recently proposed minor strengthening of C20 that rules out out-of-thin-air behaviors but allows load buffering. In contrast to existing work on verifying ARC, we do not assume acyclicity of the union of the program-order and reads-from relations. We define an interleaving operational semantics, prove its soundness with respect to (Y)C20's axiomatic semantics, and then apply any existing program logic for fine-grained interleaving concurrency, such as Iris.

翻译：我们提出了一种用于模块化验证使用宽松一致性原子内存访问原语和栅栏的程序的方法。该方法足以验证 Rust 原子引用计数算法的核心。我们首先论证了当结合一个简单的静态分析并承认一个开放子问题时，该方法相对于 C20 内存一致性模型的可靠性。随后，我们论证了即使没有任何静态分析且不作任何假设，该方法相对于 YC20 的可靠性；YC20 是 XC20 的一个轻微强化版本，而 XC20 本身是最近提出的对 C20 的一个轻微强化版本，它排除了"凭空出现"的行为但允许加载缓冲。与现有的 ARC 验证工作不同，我们并不假设程序顺序关系与读取自关系的并集是无环的。我们定义了一种交错操作语义，证明了其相对于(Y)C20 公理语义的可靠性，然后应用了任何现有的用于细粒度交错并发的程序逻辑，例如 Iris。