Happened-before
From Wikipedia, the free encyclopedia
The happened-before relation (denoted: 
) 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
and 
occur on the same process, 
if the occurrence of event preceded the occurrence of event . - If event is the sending of a message and event is the reception of the message sent in event , .
- Transitivity property: for three events , , and
, if and 
, then 
.
Unlike vector clocks, the happened-before relation is not reflexive or symmetric and, therefore, can only ensure the partial ordering of events. Specifically, implies 
but does not imply . 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).
