How can we allow read-read races between atomic and non-atomic accesses?

[RalfJung]

Currently, we document read-read races where one access is atomic and one is not to be UB. This is born out of the fact that one cannot write code in C++ that has such a race: if one creates an atomic_ref so perform atomic accesses to an object previously used non-atomically, then for as long as the atomic_ref exists, one may not use non-atomic accesses at all.

However, this is a very unfortunate limitation. First of all it means replacing a non-atomic access by an atomic one can actually introduce UB (even if there are no alignment issues), which is silly. Secondly it defies intuition. I do think we should allow such code. However, then we have to change the way we document our atomics; specifically, this part:

Rust atomics currently follow the same rules as C++20 atomics, specifically atomic_ref. Basically, creating a shared reference to one of the Rust atomic types corresponds to creating an atomic_ref in C++; the atomic_ref is destroyed when the lifetime of the shared reference ends.

My hope is that we can still use the C++ memory model, but instead of documenting which C++ library functions our Rust operations correspond to, we "link directly with the memory model" in the sense of documenting that certain Rust operations correspond to certain operations directly in the C++ model (reads/writes/RMWs). I'll have to look more closely at how the C++ standard documents the memory model to understand how this could be done; so far I've only read the CS papers that formalize this model. ;)

[gonzalobg]

The PTX memory model allows these races. The fact that these races are not allowed in C++, is not due to the C++ memory model, but due to pre-conditions in the C++ atomic and atomic_ref abstractions. These preconditions are there to enable the implementation to fake atomic memory operations using locks.

A lower-level software-exposure for these operations that guarantees "either lock-freedom or fails (to compile or at runtime)" would not need this limitation.