Proposed resolution:

This wording is relative to N5014.

1. Modify [thread.mutex.requirements.mutex.general] as indicated:

   -4- The implementation provides lock and unlock operations, as described below. For purposes of determining the existence of a data race, these behave as atomic operations ([intro.multithread]). The lock and unlock operations on a single mutex appears to occur in a single total order; for this purpose, these operations are considered as `memory_order::seq_cst` operations.

[thread.mutex.requirements.mutex.general] p4 says:

For purposes of determining the existence of a data race, these behave as atomic operations ([intro.multithread]). The lock and unlock operations on a single mutex appears to occur in a single total order.

Even for atomic operations, the precondition for ordering them in a single total order is that they must be `memory_order::seq_cst` operations, such that we can form the total order to reason.

Put aside the fact that we impose the preconditions on `unlock` and `lock`. Is this a possible total order if `lock` reads `unlock_1`, but there is a `unlock_2` between them

`unlock_1` < `unlock_2` < `lock`

First, although we have said that lock and unlock operations behave as atomic operations, and `lock` reads `unlock_1`, meaning that `unlock_1` is coherence-ordered before `lock`, however, we don't specify that they are `memory_order::seq_cst` operations, so [atomics.order] p4 doesn't apply here

Second, for every pair of atomic operations A and B on an object M, where A is coherence-ordered before B, the following four conditions are required to be satisfied by S:

• (4.1) — if A and B are both `memory_order::seq_cst` operations, then A precedes B in S; and

So, it is not helpful to decide that `unlock_1` precedes `lock` in a single total order. Similarly, excluding `unlock_1` < `unlock_2` < `lock` is not possible.

Suggested resolution:

The lock and unlock operations on a single mutex appears to occur in a single total order; for this purpose, these operations are considered as `memory_order::seq_cst` operations