Title
§[atomics.order] The total order should be intended to be a strict total order
Status
new
Section
[atomics.order]
Submitter
jim x

Created on 2025-12-09.00:00:00 last changed 3 weeks ago

Messages

Date: 2025-12-09.00:00:00

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 is

a 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:00admincreate