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

RalfJung:

However it's very hard to actually make both reads in my example return undef. One of the reads has to happen first, before any write even occurred, at which point it can only return 0 (the initial value of X and Y). Only later do we realize that actually there's a write that races with this read, now we have to... go back in time and change what the read returned?

I don't see the problem here – there's no "which read happens first" because this is a concurrent context. Each read happens in a situation where there is no synchronisation mechanism preventing another thread from writing, thus they are both raced at the time they occur (with no retroactive change being needed).

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.

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. (The only controversial part is in which specific things should cause a dependency and which specific things shouldn't.) At the hardware level, many processors also work like this: reads and writes don't occur at a single point in time but rather take some time to run, but the processors are designed to ensure that this sort of memory access always appears to start after everything it is ordered after, and always appears to finish before everything it is ordered before.

There are some examples that are interesting at the hardware level. For example (written in Rust notation, but imagine you're executing a compiled version of this on a processor):

fn example(x: &mut usize, y: &mut usize) -> usize {
    *x = 1;
    let a = *y;
    return a;
}

It is a valid implementation of this, at the hardware level, to start the performing the read of a from *y in such a way that it won't see a value currently being written to *x (and this is usually more efficient in practice than waiting for the write to actually complete) – the two are effectively "simultaneous". However, that would violate the language semantics for the code (in which the write is supposed to happen first), so the processor inserts a check for ptr::from_mut(x) == ptr::from_mut(y) and just overrides the read to return 1 (the value being written) if it succeeds. This sort of thing makes it clear why the read and write are considered unordered with respect to each other from the point of view of other threads (because if those threads tried to detect which order the accesses occurred in, they might see the read as happening before the write).

(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.)