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

RalfJung:

The argument I laid out in my blog post crucially depends on the story being expressible as actual Rust code.

We could move the validity check into the assembly block, but honestly it feels like an unnecessary (and error-prone) busy-work to create a purer "story".

RalfJung:

I look forward to your blog post and correctness argument on that subject.

Nah. I am more of practitioner and the practice shows that my line of reasoning works. I and some other people find my "story" to be satisfactory enough and it's fine if you find it vague or hand-wavy. It's not like your "correctness argument" is formally verifiable either, sure it's simpler and easier to believe, but it's still a way to convince others.

Unfortunately, in practice some of us have to deal with such grey areas (another example is IPC based on doubly mapped shared memory) and we can not wait for a more complex model to be developed. Sure, one day I could find myself in shoes of those C guys who curse compiler optimizations which break their UB-ridden code, but I consider probability of this happening sufficiently small, especially considering that no one presented even a contrived scenario in which my reasoning may fail.