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

So it turns out that this paper already proves a model in which racing an atomic read against a non-atomic write produces an undefined value rather than undefined behaviour, in a very trivial way – it makes no distinction between relaxed-atomic writes and non-atomic writes at all (they compile into the same code on every system it mentions, and none of the proofs treat non-atomic writes and relaxed writes any differently). It does make a distinction between non-atomic and relaxed-atomic reads for performance purposes, but the distinction is specific to reads (the proof basically works by proving that any cycle that they want to disallow contains a raced non-atomic read, and thus would be undefined behavior under C11 – but the fact that raced writes are also undefined behaviour under C11 is not involved in the proof).

As such, under this memory model, seqlocks should be possible to implement simply by using a relaxed-atomic read in the potentially racy step (a byte at a time for opsem purposes, but optimisable into reading all the bytes at once), because the write that it reads from can be interpreted as though it were a relaxed-atomic write (even if it were non-atomic in the source code, it would have been compiled as a relaxed-atomic write because the memory model makes no distinction between the two cases). In the situation where no race occurred, it will read the correct value; and in the situation where there was a race, it will read some arbitrary value (without violating any assumptions of the memory model proofs) which is then ignored by the program, so the actual value read doesn't matter.

That said, the paper only proves the correctness of its own compilation scheme (together with that of a few simple optimisations). Atomics have two reasons to exist (ensuring that the hardware doesn't break the semantics of the program and ensuring that compiler optimsiations don't break the semantics of the program), so in addition to showing that the memory model allows an atomic read to race against a non-atomic write (like the paper does), you would also have to show that the compiler also allows this. Fortunately, LLVM is intended to do so (its documentation specifically states that a raced read reads undef rather than producing undefined behavior), so this is another problem which turns out to already have been solved in advance.