Skip to content

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

@Eisenwave

Description

@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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions