In computer science, the happened-before relation (denoted:
\to
The happened-before relation is formally defined as the least strict partial order on events such that:
a
b
a\tob
a
b
a
b
a
a\tob
If two events happen in different isolated processes (that do not exchange messages directly or indirectly via third-party processes), then the two processes are said to be concurrent, that is neither
a\tob
b\toa
If there are other causal relationships between events in a given system, such as between the creation of a process and its first event, these relationships are also added to the definition.For example, in some programming languages such as Java, C, C++ or Rust, a happens-before edge exists if memory written to by statement A is visible to statement B, that is, if statement A completes its write before statement B starts its read.
Like all strict partial orders, the happened-before relation is transitive, irreflexive (and vacuously, asymmetric), i.e.:
\foralla,b,c
a\tob
b\toc
a\toc
a,b,c
a
b
b
c
a
c
\foralla,a\nrightarrowa
\foralla,b,
a\tob
b\nrightarrowa
a,b
a
b
b
a
Let us observe that the asymmetry property directly follows from the previous properties: by contradiction, let us suppose that
\foralla,b,
a\tob
b\toa
a\toa,
The processes that make up a distributed system have no knowledge of the happened-before relation unless they use a logical clock, like a Lamport clock or a vector clock. This allows one to design algorithms for mutual exclusion, and tasks like debugging or optimising distributed systems.