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

The usual way to formalise this sort of model is to consider reads and writes to be only partially ordered – there are certain situations that can define an ordering (with the two main ones being program order for two events that happen on the same thread, and atomics), and whenever none of these situations define an ordering between two events, the two events are considered to be unordered with respect to each other. So in the example of "two threads each read a variable the other is writing", we have the read of A being sequenced before the write of B, and the read of B being sequenced before the write of A, but the events on the two threads are unsequenced with respect to each other. As such, because the read of A is unsequenced with respect to a write of A, it is raced on – likewise, because the read of B is unsequenced with respect ot a write of B, it is raced on. This means that it is possible to determine that both are raced on without any time travel or retroactive reasoning, and they can be made to return undef as soon as it happens.

I know all that. Most models if this sort however can still be built up in some "order", adding one node after the other to the graph. You can't just magically handwave the graph into existence, after all -- the per-thread semantics has a notion of time, and you have to define which executions you consider. You get into reasoning cycles if you ignore the temporal aspect of this, that's where OOTA comes from.

ais523:

The C++ memory model (which Rust currently uses) is already formalised like this, so it wouldn't require any change in what we already have.

To my knowledge, the C++ memory model fundamentally relies on data-race UB for some of its key properties, like the DRF theorem. Nobody has demonstrated a language-level model written in that style where data races are not UB. And of course even if such a model exists, it's unclear whether it can be linked with the C++ memory model, which is required for cross-language interop.

It's easy to wave your hands and say "just do it", but if you actually get into the math, things aren't that easy. RC11 is the product of a line of work that spans more than a decade and involves a dozen of the smartest people I know. This kind of work requires a PhD-thesis-level of training and commitment.

ais523:

(With respect to the out-of-thin-air problem, I'm pretty sure that one of the solutions which has already been suggested by others as potentially solving the problem – banning cycles formed out of "program order in same thread", dependencies implied by atomics, and semantic dependencies – is the correct solution for the problem, and the only reason that it's still a problem in practice is that it's difficult to to formally define what a semantic dependency actually is.)

So, the only problem with the solution is that it doesn't actually exist?