Editing Happened-before

{{Short description|Relation between two events in computer science}}
In [[computer science]], the '''happened-before''' [[binary relation|relation]] (denoted: <math>\to \;</math>) 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 [[partially ordered set|ordering]] events based on the potential [[causal relationships|causal relationship]] of pairs of events in a concurrent system, especially [[asynchronous communication|asynchronous]] [[distributed systems]]. It was formulated by [[Leslie Lamport]].<ref>Lamport, Leslie (1978). [http://research.microsoft.com/en-us/um/people/lamport/pubs/time-clocks.pdf "Time, Clocks and the Ordering of Events in a Distributed System"], ''Communications of the ACM'', 21(7), 558-565.</ref>

The happened-before relation is formally defined as the least [[strict partial order]] on events such that:
* If events <math>a \;</math> and <math>b \;</math> occur on the same process, <math>a \to b\;</math> if the occurrence of event <math>a \;</math> preceded the occurrence of event <math>b \;</math>.
* If event <math>a \;</math> is the sending of a message and event <math>b \;</math> is the reception of the message sent in event <math>a \;</math>, <math>a \to b\;</math>.

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 <math>a \to b</math> nor <math>b \to a</math> is true.<ref>{{Cite web|title=Distributed Systems 3rd edition (2017)|url=https://www.distributed-systems.net/index.php/books/ds3/|access-date=2021-03-20|website=DISTRIBUTED-SYSTEMS.NET|language=en-US}}</ref> 

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,{{sfn|Goetz|Peierls|Bloch|Bowbeer|2006|loc=§16.1.3 The Java Memory Model in 500 words or less|pp=339-342}} 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 relation|transitive]]'', ''[[irreflexive relation|irreflexive]]'' (and vacuously, ''[[Asymmetric relation|asymmetric]]''), i.e.:
* <math>\forall a, b, c</math>, if <math>a \to b\;</math> and <math>b \to c\;</math>, then <math>a \to c\;</math> (transitivity). This means that for any three events <math>a, b, c</math>, if <math>a</math> happened before <math>b</math>, and <math>b</math> happened before <math>c</math>, then <math>a</math> must have happened before <math>c</math>.
* <math>\forall a, a \nrightarrow  a</math> (irreflexivity). This means that no event can happen before itself.
* <math>\forall a, b,</math> if <math>a \to b</math> then <math>b \nrightarrow a</math> (asymmetry). This means that for any two events <math>a, b</math>, if <math>a</math> happened before <math>b</math> then <math>b</math> cannot have happened before <math>a</math>.

Let us observe that the asymmetry property directly follows from the previous properties: by contradiction, let us suppose that <math>\forall a, b,</math> we have <math>a \to b\;</math> and <math>b \to a</math>. Then by transitivity we have <math>a \to a,</math> which contradicts irreflexivity.

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 one to design algorithms for [[mutual exclusion]], and tasks like debugging or optimising distributed systems.

==See also==
* [[Race condition]]
* [[Java memory model]]
* [[Lamport timestamps]]
* [[Logical clock]]

==Citations==
{{reflist}}

==References==
*{{cite book
 | last = Goetz
 | first = Brian
 | last2 = Peierls
 | first2 = Tim
 | last3 = Bloch
 | first3 = Joshua
 | last4 = Bowbeer
 | first4 = Joseph
 | last5 = Holmes
 | first5 = David
 | last6 = Lea
 | first6 = Doug
 | year = 2006
 | title = Java Concurrency in Practice
 | publisher = Addison Wesley
 | isbn = 0-321-34960-1
 | url = https://archive.org/details/javaconcurrencyi00goet
 }}

{{DEFAULTSORT:Happened-Before}}
[[Category:Logical clock algorithms]]
[[Category:Distributed computing problems]]
[[Category:Transitive relations]]