Created on 2025-12-09.00:00:00 last changed 3 weeks ago
The definition of (non-strict) total order in says:
In mathematics, a total order or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation ≤ on some set X, which satisfies the following for all `a`, `b` and `c` in X:
a ≤ a
if a ≤ b and b ≤ c, then a ≤ c
if a ≤ b and b ≤ a, then a = b
a ≤ b or b ≤ a
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.
Instead, the definition of a strict total order isa strict total order on a set X is a strict partial order on X in which any two distinct elements are comparable. That is, a strict total order is a binary relation < on some set X, which satisfies the following for all `a`, `b` and `c` in X:
Not a < a
if a < b then not b < a
if a < b and b < c, then a < c
if a ≠ b, then a < b or b < a
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 the definition of the (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 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. Moreover, the single total order in [atomics.order] should be a single strict total order.| History | |||
|---|---|---|---|
| Date | User | Action | Args |
| 2025-12-09 00:00:00 | admin | create | |