Happened-before relation
The happened-before relation is a strict partial order generated by process-local event order, message sending before receipt, and transitivity.
Concurrency means neither event precedes the other, not that they occur simultaneously. The relation describes potential influence within the modeled communication, not proof that one event changed another's value. [1]
In COPS, storage dependencies include client program order and reading a value written by another operation. Its model assumes inter-thread communication passes through the store; dependencies carried outside that model require separate treatment. [2]
The chosen event boundary matters: message arrival and execution of its interrupt handler need not have the same ordering. Declare which event is timestamped when interpreting a trace. [1]
Relations
Citations
- Leslie Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558-565, July 1978; pp. 559-562.
- Lloyd et al. Don't Settle for Eventual: Scalable Causal Consistency for Wide-Area Storage with COPS. SOSP 2011, sections 3, 4.4 and 5.3.
Sources & caveats
- Lamport 1978, printed p. 559: event relation and concurrency; p. 562: communication outside the modeled system.
- COPS 2011, section 3: storage-operation dependency relation and communication assumption. This record concerns distributed events, not a language-specific memory-model definition.