Include racy reads in Rust memory model with `MaybeInvalid<T>`
josh:
I would likewise expect that very few pieces of data in a program would use this kind of pseudo-cell that permits racy reads. By way of example, the Linux kernel has RCU, but the actual fraction of pointers managed by RCU is a small fraction of pointers in the kernel.
Making the kind of access a property of the location is a mistake that C made that we won't repeat -- there's no "atomic location", no "volatile location", and so also no "location that permits racy reads".
So I think you are suggesting we should introduce a new kind of read that has these semantics, while preserving the typical UB semantics for reads by default. That would greatly reduce the problems with Miri. It does nothing to fix the fact that no such model has actually been worked out in any level of detail (except for this which is a huge departure from how C++ does concurrency so we'd lose C++ interop, not to mention that the model also has various gaps and issues). In fact I don't think any model has been worked out where both "reads with UB races" and "reads with undef races" co-exist.
We haven't even solved the problems with the existing C++ model yet, and people can't agree on how they should be solved. I'm referring to the out-of-thin-air problem, which in fact is closely related to the example I posted above. Hardware people say they can't live without load buffering, and at the same time load buffering breaks deeply-rooted compiler assumptions.
Discussion in the ATmosphere