[intro.races] p4 The total order should be intended to be a strict total order

[xmh0511]

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

This is the subsequent issue of #636. The comment says

a≤b and b≤a, precisely because in a (non-strict) total order we then have a=b and they aren't two modifications. a=b there doesn't mean "the two modifications occupy the same place in the order"; it means that they are two labels for the same modification.

So, consider this example:

std::atomic<int> val;

// thread 1:
auto r = val.load(relaxed); // #1
val.store(1,relaxed); // #2

// thread 2:
val.fetch_add(1,relaxed); // #3

To determine whether this is a valid path: #3 reads #2 and #1 reads #3, we should check whether this path can form a valid modification order. According to [intro.races] p13

If a value computation A of an atomic object M happens before an operation B that modifies M, then A takes its value from a side effect X on M, where X precedes B in the modification order of M.

If #1 reads #3, this implies #3 precedes #2 in the modification order. Then, in the assumption, we say #3 reads #2, which together forms the below modification order

#3 ≤ #2 ≤ #3

According to the second bullet of (non-strict) total order, we can get #3 ≤ #3, which is also valid according to the first bullet. Then we instead use the third bullet to claim #3 = #2 in that valid total order. However, #3 and #2 are different modifications, so that the total order is not possible, which is quite indirect. It's a bit overcomplicated for reasoning.

Moreover, (non-strict) single total says

any two elements are comparable

It includes that an element is also comparable with itself. This is not close to what we want for the definition of modification order. Instead, the definition of strict total order says

any two distinct elements are comparable

This is what we want.

Moreover, if we use the definition of strict total order, the above modification order would be

#3 < #2 < #3

This is an invalid strict total order, so the assumption of execution is not possible.

Suggested Resolution:

A strict total order is more direct in expressing what we want. It doesn't exist the case where it is only explained by a non-strict total order, but not by a strict total order, within the bounds of modification order.