Created on 2025-12-09.00:00:00 last changed 2 weeks ago
[ 2026-02-18; Reflector poll. ]
Set priority to 4 and status to SG1 after reflector poll.
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, when we get `#3 = #2` according to the non-strict total order in the above example, it's unclear what `=` means here, since we didn't define what `=` means between two modifications in the modification order. Whether the total order is valid depends on how `=` intended to mean for two modifications in a non-strict total order. This is quite indirect and is a bit overcomplicated for reasoning.
The definition of strict single total order saysany 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 |
| 2026-02-18 14:45:45 | admin | set | messages: + msg15936 |
| 2026-02-18 14:45:45 | admin | set | status: new -> open |
| 2025-12-09 00:00:00 | admin | create | |