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

TL;DR

This paper introduces a modular verification approach for Rust's ARC algorithm under relaxed memory models, ensuring correctness without assuming acyclicity, and applies existing concurrency logic for validation.

Contribution

It presents a novel modular verification method for Rust's ARC that works under relaxed memory models without assuming acyclicity, extending prior verification techniques.

Findings

Verification is sound for C20 and YC20 memory models.

The approach does not require acyclicity of program relations.

It successfully applies existing program logic to verify Rust's ARC.

Abstract

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.