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

ais523:

I've thought quite a lot about this, and I'm pretty sure that the correct model is along the lines of "a data race for which the value read affects observable program behaviour is undefined behaviour"

Yes that's exactly what this thread is about: racy reads return undef. undef is a value where if the program behavior ever depends on what the value is, that's UB. (poison would work just as well for us here.)

However it's very hard to actually make both reads in my example return undef. One of the reads has to happen first, before any write even occurred, at which point it can only return 0 (the initial value of X and Y). Only later do we realize that actually there's a write that races with this read, now we have to... go back in time and change what the read returned? That's not even a meaningful thing to say. In the current semantics, we can just say "UB" at this point and we're fine. But in a world where data-races are not always UB, we need an odd form of time-traveling semantics. That can be done, but it is exceedingly complicated and nobody has managed to actually work with such a model so far.

You can also entirely forget about having a tool like Miri for such a semantics. So we can add that to the list of downsides of this model. (Miri of course already has the same problem for the variant of this program where the two loads are Ordering::Relaxed. But given that only a tiny fraction of reads in any given program use that ordering, I think it is a very different situation if we have that problem for all reads vs. only for a few of them.) Miri would become largely useless for finding data races if we adopted this model.