An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model.

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.