Happened-before

The happened-before relation (denoted: $o$) is a means of ordering events based on the causal relationship of two events in asynchronous distributed systems. It was formulated by Leslie Lamport.

The happened-before relation is formally defined as:
* If events $a\; ;$ and $b\; ;$ occur on the same process, $a\; o\; 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\; o\; b$.
* Transitivity property: for three events $a\; ;$, $b\; ;$, and $c\; ;$, if $a\; o\; b$ and $b\; o\; c$, then $a\; o\; c$.

The happened-before relation is "irreflexive" and "antisymmetric", i.e.:
* $forall\; a,\; a\; ot\; o\; a$ (irreflexivity) ;
* $forall\; a,\; b$ such that $a\; eq\; b$, if $a\; o\; b$ then $b\; ot\; o\; 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.

ee also

* Java Memory Model