Happened-before

The happened-before relation (denoted: $\to$ ) 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 \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$ .

Unlike vector clocks, the happened-before relation is not reflexive or symmetric and, therefore, can only ensure the partial ordering of events. Specifically,

a \to b

implies

time(a) < time(b) \;

but

time(a) < time(b) \;

does not imply

a \to b

. In order to formulate total ordering of events, an algorithm such as vector clocks must be used.

The happened-before relationship is used in time stamping messages (Lamport timestamps) and in building logical clocks (Lamport clocks).

Distributed systems

Happened-Before | Algoritme van Lamport

Gourt Home::Gourt :: Happened-before