Our concurrency memory model (inherited from C++20) is incompatible with x86

[RalfJung]

See https://cplusplus.github.io/LWG/lwg-active.html#3941 for details. Thanks @orilahav for pointing this out to me.

[chorman0773]

Having read the issue, I'm not sure that it's incompatible. It's just that it's universally miscompiled. The issue is that compiling it properly will make it a stupid amount slower (and I'm not sure C++ users will appreciate the perf regresssiom).

Specifically, putting an mfence after each mov for a SeqCst load would be sufficient, as would using lock cmpxchg/cmpxchg8b on targets without SSE. Though this means that non-sse can't compile any SeqCst loads in a manner that is compatible with accessing read-only memory.

[taiki-e]

Though this means that non-sse can't compile any SeqCst loads in a manner that is compatible with accessing read-only memory.

This problem should not occur as LLVM can emit a lock or dword ptr [esp], 0, as it already does for SeqCst fences and 64-bit SeqCst stores in environments without SSE: https://godbolt.org/z/qPYqx9nda

[RalfJung]

Well, it is incompatible with the intended lowering. Changing the lowering is the wrong fix for this.

[chorman0773]

Well without changing our memory model or bugging WG-21, I'm not sure what the "right fix" would be.
It's entirely possible that WG-21 considered this sort of change (Not the precise one or gcc/clang/msvc would all know) and accepted the memory model with that in mind, in which case, at least from the C++ side, changing the lowering would be theright fix.

[RalfJung]

I like this comment from the report

[ Meta-observation from a small off-line discussion that may be relevant to how we phrase the resolution here: The fact that nobody noticed this for a very long time, and implementers were not bothered by it, suggests that the audience for this part of the standard is nearly empty. We conjecture that implementers actually rely on atomics mappings generated by memory model experts, who are more interested in formal models than standardese. A more formal description is likely to increase the size of the audience, and would definitely ease verification and reduce the probability of mistakes like this.]

I definitely agree that just defining the relevant orders and consistency axioms would be much better than trying to circumscribe them in standardese. Even if the definition is carried out in English, as long as its translation into formal syntax is clear, that seems much better than the current approach the C++ standard is taking.

It's entirely possible that WG-21 considered this sort of change (Not the precise one or gcc/clang/msvc would all know) and accepted the memory model with that in mind, in which case, at least from the C++ side, changing the lowering would be theright fix.

It's very clear from the document I linked above that this is a mistake they made when translating the formal notation from the paper into plain English:

The problem here is an error during the attempt to simplify and translate plv.mpi-sws.org/scfix/paper.pdf to standardese. There is no known issue with the underlying paper.

[arielb1]

It's very clear from the document I linked above that this is a mistake they made when translating the formal notation from the paper into plain English:

Do they know what the error is?

[RalfJung]

Yes, please read the document linked in the OP.

[arielb1]

The OP doesn't seem to have a "Proposed resolution"

[RalfJung]

No, but it describes the error.

Currently, we require that the sequential consistency order S is consistent with the extended coherence order, which includes "reads before" and "reads from". This may require sc reads to be consistently ordered even if they see non-sc writes. This is not enforced by some "fence-after-store"/"trailing fence" sc implementations, notably on X86. It may also be violated by compiler transformations that eliminate a sequentially consistent load after a store into the same location, e.g. on sequentially consistent hardware.

The proposed resolution is to follow exactly what the paper suggests (minus "(po \cup rf) acyclic").

[arielb1]

So "coherence-ordered" is supposed to be the same as the paper's "psc", but it's just written in standartese that has a completely different meaning?

[RalfJung]

I don't know what the intended correspondence between paper and standard is, sorry. Maybe @orilahav can help with that.

[arielb1]

Reading the paper I completely understand why the person that translated the paper didn't like the "seqcst-order is inconsistent with happens before" concept.

[RalfJung]

The consequences of memory model choices can be quite counter-intuitive. That's why we need formalizations of these models. Clearly we want to be able to compile atomics to x86 in the obvious way, and therefore we must accept this concept even if we don't like it.

[arielb1]

I'm actually not sure the "add barriers solution" would be that bad to Rust, which doesn't use SeqCst reads much. Tho "change the model" is probably better.

[RalfJung]

I don't think we should make SC reads in Rust surprisingly more expensive than in C++. Also we have to consider compatibility with C++ whenever we share memory.