fbpx
Wikipedia

Happened-before

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.[1]

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.[2]

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,[3] 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 the previous properties: by contradiction, let us suppose that we have and . Then by transitivity we have 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 edit

Citations edit

  1. ^ Lamport, Leslie (1978). "Time, Clocks and the Ordering of Events in a Distributed System", Communications of the ACM, 21(7), 558-565.
  2. ^ "Distributed Systems 3rd edition (2017)". DISTRIBUTED-SYSTEMS.NET. Retrieved 2021-03-20.
  3. ^ Goetz et al. 2006, pp. 339–342, §16.1.3 The Java Memory Model in 500 words or less.

References edit

  • Goetz, Brian; Peierls, Tim; Bloch, Joshua; Bowbeer, Joseph; Holmes, David; Lea, Doug (2006). Java Concurrency in Practice. Addison Wesley. ISBN 0-321-34960-1.

happened, before, computer, science, happened, before, relation, denoted, displaystyle, relation, between, result, events, such, that, event, should, happen, before, another, event, result, must, reflect, that, even, those, events, reality, executed, order, us. In computer science the happened before relation denoted displaystyle to 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 1 The happened before relation is formally defined as the least strict partial order on events such that If events a displaystyle a and b displaystyle b occur on the same process a b displaystyle a to b if the occurrence of event a displaystyle a preceded the occurrence of event b displaystyle b If event a displaystyle a is the sending of a message and event b displaystyle b is the reception of the message sent in event a displaystyle a a b displaystyle a to b 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 a b displaystyle a to b nor b a displaystyle b to a is true 2 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 3 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 a b c displaystyle forall a b c if a b displaystyle a to b and b c displaystyle b to c then a c displaystyle a to c transitivity This means that for any three events a b c displaystyle a b c if a displaystyle a happened before b displaystyle b and b displaystyle b happened before c displaystyle c then a displaystyle a must have happened before c displaystyle c a a a displaystyle forall a a nrightarrow a irreflexivity This means that no event can happen before itself a b displaystyle forall a b if a b displaystyle a to b then b a displaystyle b nrightarrow a asymmetry This means that for any two events a b displaystyle a b if a displaystyle a happened before b displaystyle b then b displaystyle b cannot have happened before a displaystyle a Let us observe that the asymmetry property directly follows from the previous properties by contradiction let us suppose that a b displaystyle forall a b we have a b displaystyle a to b and b a displaystyle b to a Then by transitivity we have a a displaystyle a to a 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 editRace condition Java Memory Model Lamport timestamps Logical clockCitations edit Lamport Leslie 1978 Time Clocks and the Ordering of Events in a Distributed System Communications of the ACM 21 7 558 565 Distributed Systems 3rd edition 2017 DISTRIBUTED SYSTEMS NET Retrieved 2021 03 20 Goetz et al 2006 pp 339 342 16 1 3 The Java Memory Model in 500 words or less References editGoetz Brian Peierls Tim Bloch Joshua Bowbeer Joseph Holmes David Lea Doug 2006 Java Concurrency in Practice Addison Wesley ISBN 0 321 34960 1 Retrieved from https en wikipedia org w index php title Happened before amp oldid 1197656002, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.