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

ais523:

to allow races of atomic reads against non-atomic writes (i.e. effectively LLVM's model)

That is not LLVM's model. LLVM's model is that all read-write races are allowed. So this includes non-atomic reads against atomic writes, and non-atomic reads against non-atomic writes. (Well, LLVM's model is something like that. Not even LLVM themselves know what their model is, so we probably shouldn't use the term "LLVM's model", though I am guilty of that myself.)

That's still an interesting claim you are making, if it is correct. Unfortunately I lack the time to verify those proofs.