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

By: Bart Jacobs, Justus Fasse

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 with respect to the C20 memory consistency model, then with respect to YC20, a minor strengthening of XC20. 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.

Keywords

Relaxed Memory Consistency, Separation Logic, Modular Verification, Rust, Atomic Reference Counting

Cite as:

Bart Jacobs, Justus Fasse, “An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-13, doi:10.5381/jot.2026.25.1.a3.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn