[intro.races] p4 The determination of a modification order forms a cycle dependency on the well-defined behavior

[xmh0511]

Full name of submitter (unless configured in github; will be published with the issue): Jim X

[intro.races] p4 says:

All modifications to a particular atomic object M occur in some particular total order, called the modification order of M.

To prove the program correct, we should determine all possible modification order of an atomic object, which relies on the observation of the load together with other coherent requirements according to [intro.races], the observation depends on whether the program is well-defined, otherwise, the standard imposes no requirement.

Consider this example:

int v = 0;
std::atomic<int> a = {0};
//thread 1:
v = 1;
a.exchange(1);  // #1

// thread 2:
a.exchange(2); // #2
assert(a.load() != 0 );  // #3
auto r = v;

this program is data-race-free if #2 or #3 reads the value written by #1, however, in this example, we should prove it by forming the possible modification orders, the value read by #2 or #3 should be observed to determine the possible modification orders, this observation depends on this program is well-defined, which in turn, depends on whether the operations to v is data-race or not, which in turn, depends on whether #1 synchronizes with #2, which is circle dependency. So, form all possible modification orders of a to prove the program correct stuck into the circle of dependency.

Suggested Resolution

If ignore the data-race caused by conflict operation to v, the possible modification order to a should be:

1. 0 < 1 < 2
2. 0 < 2 < 1

the possible value read at #3 is restricted by these possible modification orders and [intro.races] p18. Shall we say the modification order of an atomic object can always form regardless of whether the program is well-defined or not? In other words, the first modification order interprets why the program may be an undefined behavior, but since the program has UB, how is this modification order inferred according to the observation that is in the UB program?

[frederick-vs-ja]

Sounds like a more general issue - some rule affects the well-definedness of the program, but the rule itself is applied only if the program is well-defined?

If there's actually an issue, I think there's something wrong in [intro.abstract] but not in [intro.races] p4.

[xmh0511]

Sounds like a more general issue - some rule affects the well-definedness of the program, but the rule itself is applied only if the program is well-defined?

Yeap, this is the subject of this issue.

[t3nsor]

Sounds like a more general issue - some rule affects the well-definedness of the program, but the rule itself is applied only if the program is well-defined?

If there's actually an issue, I think there's something wrong in [intro.abstract] but not in [intro.races] p4.

Yes, I don't see any fundamental difference between this issue and:

int x = 1;
std::cout << 1/x;

Whether the division in the second statement has defined behavior depends on the value of x at that point. But the value of x depends on the behavior of the first statement, and the behavior of the first statement depends on whether the program has defined behavior, because if the program has undefined behavior then there are no constraints on what the first statement (or anything else in the program) does. So, is there a circular dependency here?

Maybe this is a core issue, but (just my personal opinion) I think it's unlikely that anyone in CWG is going to volunteer to write the wording to fix it. I assume folks know how to squint and infer the intended meaning of the standard. There are implicit operational semantics that are poorly described by the current wording but which are mostly understood anyway.

There is actually a paper in the works that proposes to clarify the operational semantics, but the details are currently committee-private. You might see it in the next mailing. If that doesn't materialize, you could of course write your own paper.