The happened-before relation is formally defined as:

• 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$.
• Transitivity property: for three events $a\; ;$, $b\; ;$, and $c\; ;$, if $a\; to\; b$ and $b\; to\; c$, then $a\; to\; c$.

The happened-before relation is irreflexive and antisymmetric, i.e.:

• $forall\; a,\; a\; notto\; a$ (irreflexivity) ;
• $forall\; a,\; b$ such that $a\; neq\; b$, if $a\; to\; b$ then $b\; notto\; 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.

See also

• Java Memory Model