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).