Happened-before

In computer science, the happened-before relation (denoted: $\to \;$ ) is a means of ordering events based on the potential causal relationship of pairs of events in a concurrent system, especially asynchronous distributed systems. It was formulated by Leslie Lamport.^[1]

The happened-before relation is formally defined as the least strict partial order on events such that:

If events $a \;$ and $b \;$ occur on the same process, $a \to b\;$ if the occurrence of event $a \;$ preceded the occurrence of event $b \;$ .
If event $a \;$ is the sending of a message and event $b \;$ is the reception of the message sent in event $a \;$ , $a \to b\;$ .

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.

Like all strict partial orders, the happened-before relation is transitive, irreflexive and antisymmetric, i.e.:

$\forall a, b, c$ , if $a \to b\;$ and $b \to c\;$ , then $a \to c\;$ (transitivity) ;
$\forall a, a \nrightarrow a$ (irreflexivity) ;
$\forall a, b,$ if $a \to b\;$ then $b \nrightarrow a$ (antisymmetry).

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 to design algorithms for mutual exclusion and tasks like debugging or optimising distributed systems.

References

^ Lamport, Leslie (1978). "Time, Clocks and the Ordering of Events in a Distributed System", Communications of the ACM, 21(7), 558-565.

Happened-before

See also

References