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

RalfJung:

I have come up with counterexamples to multiple proposals that involve the program predicting the future (e.g. here and here).

I find the first example here really interesting because I think it demonstrates a difference between two different sorts of future-prediction / angelic choice (and also think that it's effectively the same situation as the sequence-lock situation being discussed in this thread).

From my point of view, the reordering of the let b and let x lines in the the first example is allowed even with angelic choice being used , and the reason is that the sequence of events is as follows:

• x is created from a pointer using exposed provenance. For the time being, the provenance is opaque, in the sense that the compiler's behaviour does not depend on it.
• b is chosen non-deterministically.
• Depending on the value of b, x is offset. Its provenance is still opaque (but the same as what it was previously).
• x is dereferenced. At this point, we determine what its provenance must have been, on the basis of which address is being accessed. It is considered to have had that provenance all along (e.g. trying to access a different allocation through a copy of x would be undefined behavior).

Or in other words, I don't see the angelic choices as being made immediately. Rather, I think that sort of choice works like variables in Prolog: initially nothing is known about them, as they are used it places more constraints on what they are, if the constraints can't be fulfilled simultaneously you get a failure (in Prolog) or undefined behavior (in Rust semantics). For people who haven't seen Prolog before, it lets you write this sort of program:

A = B,
write(B),
A = 2,
write(B).

and get an output saying that B's value is unknown from the first write, and an output saying that B is 2 from the second write. (The program is evaluated in order from start to end, and yet learning more about A nonetheless lets us know more about what B is/was, without any futher information being given about B directly.)

The basic idea is that just as a Prolog implementation can't make assumptions about the value of B until it sees some evidence about what the value is, a Rust compiler can't make assumptions about what provenance is obtained from from_exposed_provenance until it sees the pointer being dereferenced in a way that puts constraints on the provenance, or about whether or not an inline-assembly block actually read memory until it can prove that the read would have been a race.

I think that this is conceptually the sort of reasoning that people want to apply to both the seqlock case (where we determine whether or not we have read from the memory, depending on whether we subsequently treat the resulting value as initialised or not) and the exposed-provenance case (where we determine which provenance the pointer had, based on which addresses it is subsequently used to access). That said, I am not convinced that this sort of reasoning is, in the abstract, always correct – based on my previous attempts to prove seqlocks correct, I suspect that it's almost right, but that merely using this Prolog-style reasoning isn't automatically enough to prove the code sound, there may be other constraints too which haven't been formalised yet.

Or in other words, this sort of argument from opaqueness is probably the most natural approach to solve this sort of problem (as opposed to doing things like changing the memory model, which is easier to prove correct), and many people seem to intuitively feel that it is obviously correct, but more effort will be needed to determine whether it actually does work, and to formally prove why. (There's an attractive informal argument why it works – while the angelically-determined information is opaque and so the compiler has no evidence to constrain it, it can't make optimisations that depend on its properties – but this argument is hard to formalize properly.)