Include racy reads in Rust memory model with `MaybeInvalid<T>`

RalfJung:

Oh it definitely is.

For it we would need to formally prove equivalence between the told "story" and the respective asm! block. Without it we are still in the realm of hand-waving.

RalfJung:

I am sure I can come up with counterexamples

You should've started with it without assuming my dismissal. A good counter-example can eliminate a lot of unnecessary back-and-forth discussions (like MADV_FREE in the context of uninitialized memory).

RalfJung:

consider those accesses to be relaxed bytewise atomic

Great, now you potentially break CPU soundness requirements (at least on Intel) which forbid simultaneous differently sized atomic operations on the same memory. This restriction may apply only to synchronizing atomic operations, IIRC the Intel manual was somewhat vague in this regard and Linux just ignores it, but still.

UDP: Ah, you mean that both reads and writes should be bytwise atomic.