-
Notifications
You must be signed in to change notification settings - Fork 7
Description
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.
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.