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

Bart Jacobs, Justus Fasse

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 co…