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

newpavlov: > It's not like your "correctness argument" is formally verifiable either, Oh it definitely is. newpavlov: > Nah. I am more of practitioner and the practice shows that my line of reasoning works. I am sure I can come up with counterexamples (EDIT: to the general approach of allowing the asm story to predict the future). But then you'll dismiss them as artificial. Obviously for code you write you get to choose whatever tradeoffs you prefer for how thorough you want to be with your correctness arguments. But for project-official guidance I think we should have pretty high standards. FWIW, I think the reason that "seqlock with inline asm for the data reads and writes" works in practice is that there is another story, one that actually works in my framework (assuming a language extension to Rust that we'll hopefully get one day): consider those accesses to be relaxed bytewise atomic. I don't know if your intended implementation uses inline asm for both the read and the write path, but if it does, then I'd say your code is correct, just your story / correctness argument isn't.