Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Happened-before
Summary
In computer science, the happened-before relation (denoted: ) is a relation between the result of two events, such that if one event should happen before another event, the result must reflect that, even if those events are in reality executed out of order (usually to optimize program flow). This involves ordering events based on the potential causal relationship of pairs of events in a concurrent system, especially asynchronous distributed systems. It was formulated by Leslie Lamport.
The happened-before relation is formally defined as the least strict partial order on events such that:
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 , .
If two events happen in different isolated processes (that do not exchange messages directly or indirectly via third-party processes), then the two processes are said to be concurrent, that is neither nor is true.
If there are other causal relationships between events in a given system, such as between the creation of a process and its first event, these relationships are also added to the definition.
For example, in some programming languages such as Java, C, C++ or Rust, a happens-before edge exists if memory written to by statement A is visible to statement B, that is, if statement A completes its write before statement B starts its read.
Like all strict partial orders, the happened-before relation is transitive, irreflexive (and vacuously, asymmetric), i.e.:
if and , then (transitivity). This means that for any three events , if happened before , and happened before , then must have happened before .
(irreflexivity). This means that no event can happen before itself.
if then (asymmetry). This means that for any two events , if happened before then cannot have happened before .
Let us observe that the asymmetry property directly follows from from the previous properties: by contradiction, let us suppose that we have and .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.