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

RalfJung:

The return T::default() is wrong though since the asm code may return a different value.

True. There should be some source of nondet (demonic permitted)... well for any T that can be constructed from byte array (like std::vec::Vec<u8>, impl bytemuck::AnyBitPattern or impl arbitrary::Arbitrary) there is one: allocate a few blocks and use the pointer addresses to generate the instance.

RalfJung:

but for the story to be valid the asm code has to perform at least as much synchronization as the story.

I believe the asm code must do similar synchronization (including the Release fence between data read and check if someone wrote in parallel, which happens here on automatic unlock), and will leave that question to whoever writes the actual implementation.

RalfJung:

That has a different size than T so this doesn't literally work, but I guess we could imagine that the RwLock state is stored out-of-band.

Notably, SeqLock is also T plus a counter integer so it should work out.