Weak memory emulation does not respect C++20 SCfix

[RalfJung]

Our weak memory emulation does not respect the C++20 SCfix, so we could sometimes produce values that are not actually possible on the real machine. This can lead to false UB reports when SeqCst fences are used.

Unfortunately, no literature exists at the time of writing which proposes an implementable and C++20-compatible relaxed memory model that supports all atomic operation existing in Rust.

[SabrinaJewson]

I believe that false positives can be produced even when fences are not used. In particular, consider this code:

static X: AtomicBool = AtomicBool::new(false);
static Y: AtomicBool = AtomicBool::new(false);

let a = thread::spawn(|| X.store(true, Relaxed));
let b = thread::spawn(|| Y.store(true, Relaxed));
let c = thread::spawn(|| { while !X.load(SeqCst) {} Y.load(SeqCst) });
let d = thread::spawn(|| { while !Y.load(SeqCst) {} X.load(SeqCst) });

a.join().unwrap();
b.join().unwrap();
let c = c.join().unwrap();
let d = d.join().unwrap();

assert!(c || d);

playground, I had to loop it to get Miri to fail

Currently, Miri can panic on it, but by the C++20 rules I don’t think it is allowed to. The execution of the code can be represented with this diagram:

     a        static X         c               d        static Y         b
╭─────────╮   ┌───────┐   ╭─────────╮     ╭─────────╮   ┌───────┐   ╭─────────╮
│ store X ├─┐ │ false │ ┏━→ load X  │     │ load Y  ←━┓ │ false │ ┌─┤ store Y │
╰─────────╯ │ └───────┘ ┃ ╰────╥────╯     ╰────╥────╯ ┃ └───────┘ │ ╰─────────╯
            └─┬───────┐ ┃ ╭────⇓────╮     ╭────⇓────╮ ┃ ┌───────┬─┘
              │ true  ┝━┛ │ load Y  ┝━? ?━┥ load X  │ ┗━┥ true  │
              └───────┘   ╰─────────╯     ╰─────────╯   └───────┘

Using [thread name]-[operation number] notation to refer to each operation, the logic is as follows:

• Either c-0 precedes d-1 in S, or d-0 precedes c-1 in S, or both: I will call the preceding operation A, the succeeding operation B, and the relevant memory location (either X or Y) M.
• If B were to load false from M, it would be coherence-ordered before A.
  • This is because “there exists an atomic modification X of M such that [B] is coherence-ordered before X and X is coherence-ordered before [A]”, where X is the Relaxed store of true to M.
    • B is coherence-ordered before X because “[B] and [X] are not the same atomic read-modify-write operation, and there exists an atomic modification [Y] of M such that [B] reads the value stored by [Y] and [Y] precedes [X] in the modification order of M”, where Y is just the initial value of M
    • X is coherence-ordered before A because “[X] is a modification, and [A] reads the value stored by [X]” (i.e. true)
• However, if B would be coherence-ordered before A then it would have to precede A in S.
  • This is because “for every pair of atomic operations [B] and [A] on an object M, where [B] is coherence-ordered before [A] […] if [B] and [A] are both [SeqCst] operations, then [B] precedes [A] in S”.
• But since we already know A precedes B in S, such an execution where B would load false from M is not possible.
• Therefore, at least one of c-1 or d-1 must load true from M.

[RalfJung]

Cc @cbeuw would be great if you could take a look at the above. :)

[RalfJung]

I will call the preceding operation A, the succeeding operation B

Here do you mean "succeeding" as in "success" or as in "second"?

[SabrinaJewson]

As in “second”.

[RalfJung]

Okay, makes sense. And thanks for the detailed description! I don't know the C++ memory model well enough to check if this is all according to spec, but the explanation made sense in itself. :)

[cbeuw]

@SabrinaJewson I think the logic deduction is a bit off. You started with the assumption of B loading false, reached a contradiction, thus proving that B cannot load false. But surely you have proved that B cannot load false for all possible values of B, and not "all possible values of B cannot simultaneously load false"?. Suppose A is c-0 and B is d-1, then you have shown that d-1 cannot load false regardless of what c-1 loads (since your proof does not even name it). So what you actually proved is that neither c-1 or d-1 can load false. Both must be true.

I actually do agree with your conclusion that at least one of them must be true though:

• Assume d-1:X.load reads false (without assuming the S edge between c and d)
• Since d-1:X.load reads false, it is coherence-ordered before a-0:X.store(true) (d-1:X.load "reads-before" a-0:X.store(true))
• Since c-0:X.load reads true, a-0:X.store(true) is coherence-ordered before it.
• So d-1:X.load is coherence-ordered before c-0:X.load
• So d-1:X.load precedes c-0:X.load in S, since they are coherence-ordered before and both SC
• So we have S as d-0:Y.load, d-1:X.load, c-0:X.load, c-1:Y.load
• Now further assume c-1:Y.load reads false
• Through the same deduction you can get c-1:Y.load precedes d-0:Y.load in S, which is a contradiction
• Therefore c-1:Y.load must read true

So we get d-1:X.load reading false implies c-1:Y.load reading true, and the reverse obviously stands too, so d-1:X.load and c-1:Y.load cannot both be false.

cppmem says all 4 combinations of (c-1, d-1) can occur under C++11, so this appears to be due to SCFix indeed.

int main() {
  atomic_int x=0; atomic_int y=0;
  x.store(0, memory_order_relaxed); y.store(0, memory_order_relaxed);
  {{{ { x.store(1,memory_order_relaxed); }
  ||| { y.store(1,memory_order_relaxed); }
  ||| { x.load(memory_order_seq_cst).readsvalue(1); y.load(memory_order_seq_cst); }   
  ||| { y.load(memory_order_seq_cst).readsvalue(1); x.load(memory_order_seq_cst); } }}}
  return 0;
}

The crux of the issue here is that if you have two SC loads and a non-SC store, the first SC load doesn't see the store and the second one sees it, then under C++20 the first load must precede the second load in S, whereas previously this is not necessarily the case (unless covered by other coherence rules, such as if the two loads happen-before each other)

[cbeuw]

This is not hard to fix I think. Basically, if there's an SC load that reads from any store, then another SC load later in S cannot read before that store. This is because read from gives you a cob, read before gives you a cob, cob + cob is a cob, and a cob between SCs gives you an extra S edge, so we can't create the read before edge on the second load, otherwise we create a backwards S edge. When going through the store buffer, we need to check if the current store element has ever been SC loaded. If so, then we need to stop the search.

This is very similar to the basic Coherent-RR actually, which states that if two loads on the same location happen before each other, then the later load cannot read a value earlier in MO than what the first load saw. Except in C++20, it's both hb and S.

The remaining question is whether this is consistent with the standard. I don't have the ability to prove anything like the author did, though the modification on the race detector side for the release sequence changes seem to be in the same boat. In any case, since I'm restricting the "outdatedness" of values a load can see, the new possible behaviours is a strict subset of the current implementation, so it can't be more unsound than now.

[RalfJung]

Yeah, if this can definitely only rule out some behaviors Miri currently produces (and not add more behavior), and if it rules out some behavior that we agree is wrong, then we should do it even if it also rules out other behavior that would be allowed (we already have plenty of that).

[RalfJung]

All right, that particular issue should be fixed by #2512. :) The wider problem of not respecting SC fences properly remains, though.

This is somewhat surprising since, to my knowledge, SC fences are actually much more well-behaved in C++20 than SC accesses. For example, the operational Promising Semantics model supports SC fences but not SC accesses. I wonder if we can copy the SC fence approach from the promising semantics, or are there too many other differences that make this impractical?

[cbeuw]

SC fences are better behaved. Adapting Promising Semantics' SC fences is possible and can actually simplify our code. The bit I'm not fully comfortable with is the interaction between SC fences and SC accesses, which are fairly intertwined.

I'm having another look at the C++20 SC definitions. I think the new wording is relatively friendly to translate to operational models since it's worded in terms of "if this happened, then there's an S edge", so all we need to focus on is "don't create a backwards S edge by reading the wrong store", since we always have S naturally as the operational steps. But because coherence-ordered before is transitive, it might be tricky to cover all cases.