[intro.execution] Sequenced before is implied but not stated to be irreflexive

[Eisenwave]

Full name of submitter: Jan Schultke

Reference (section label): [intro.execution] p8

Issue description:

The sequenced before relation is implied to be irreflexive:

Given any two evaluations A and B, if A is sequenced before B [...], then the execution of A shall precede the execution of B.

- [intro.execution] p8

According to the Oxford dictionary, precede (verb) means:

to happen before something or come before something/somebody in order

Intuitively, an execution cannot happen before itself; it only happens at a single point in time. If an execution cannot precede itself, and thus an evaluation cannot be sequenced before itself, sequenced before is irreflexive. This makes it a strict partial order.

Formally, a lack of irreflexivity implies that evaluations can be sequenced before themselves. This would violate [intro.races] p10, which requires the happens before relation to be acyclic. An evaluation sequenced before itself would be an evaluation which happens before itself, which would be a cycle of length 1.

Suggested resolution:

 Sequenced before is an
+irreflexive,
 asymmetric, transitive, pair-wise relation between evaluations executed by a single thread ([intro.multithread]),
 which induces a
+strict
 partial order among those evaluations.

[Eisenwave]

I've been informed that asymmetry is not the same as anti-symmetry, and it implies irreflexivity already. This means that there is no ambiguity and the issue is purely editorial.

See https://github.com/cplusplus/draft/pull/6434