Happened-before

From Wikipedia, the free encyclopedia

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.

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

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