Happens-before

Lamport combines process-local order, sending before receiving the same message, and transitivity. Events unordered in either direction are concurrent rather than assigned a known causal direction.

Logical clocks can respect that order: if A precedes B, its clock value is smaller. The converse does not follow; numerical timestamps can also order events with no happens-before relation.

References: [1]

Language memory models apply related ordering to memory actions. Java defines edges for unlocking and later locking the same monitor, thread lifecycle operations and volatile accesses.

Such synchronization can publish one thread’s data to another. The reasoning must identify an actual synchronization chain, not merely assume that a thread probably ran later.

References: [2]

The C++ draft builds happens-before from sequenced-before, synchronization and transitivity. A release store and an acquire load taking its value can synchronize; relaxed atomics are not equivalent publication barriers merely because they are atomic.

Languages differ in the consequences of races. C++ makes data races meeting its definition undefined behavior, so Java’s guarantees cannot simply be transferred to C++ code.

References: [3]