Happens-before: causality is a partial order

Happens-before is the smallest transitive relation containing program order inside each process and every message send before its matching receive. It describes potential causal influence, not wall-clock order, network arrival order, or immediate global visibility.

If neither a -> b nor b -> a, the events are concurrent in the causal model. That means incomparable, not necessarily simultaneous. Enforcing causal delivery additionally requires metadata, buffering, retransmission, and bounded gap handling.

Prerequisites and model

• Each event belongs to a process and every modeled receive is matched to one concrete send.
• Process-local order is meaningful; a retry is a new transport event carrying the original operation identity.
• The network may delay, reorder, duplicate, or lose messages, so delivery and deduplication are separate mechanisms.

Correctness claims and invariants

• HB-C1. a -> b follows from same-process order, a send before its matching receive, or transitive closure.
• HB-C2. Concurrency is incomparability: neither event happens before the other; physical timestamps cannot prove that relation.
• HB-C3. Lamport clocks guarantee a -> b => L(a) < L(b), but the converse is false.
• HB-C4. A (clock, process-id) tie-break is a total-order extension for presentation, not new causality.
• HB-C5. A causal consumer withholds an effect whose declared predecessor is missing, then fetches, receives, or expires the gap under policy.
• HB-C6. Causal metadata does not suppress a repeated side effect; retries need stable operation identity or idempotence.

What the scenarios prove

• Program order (local-order): Two sequential events in one process are ordered without a message.

• Send before receive (message-edge): Transport delay does not erase the causal send-to-receive edge.

• Transitive causal chain (transitive-chain): Receive, local work, and a new send compose one causal path.

• Causally concurrent events (concurrent-events): Independent events have no path in either direction even if displayed in an order.

• Lamport converse is false (scalar-converse): Ordered scalar values do not prove ancestry.

• Missing predecessor buffer (delayed-dependency): A dependent effect is withheld until its missing predecessor arrives.

• Retry still needs dedupe (retry-duplicate): Causal order can be correct while a repeated business effect is wrong.

Failure, concurrency, and retry traps

• Host wall clocks can invert causality when clocks skew or move backward.
• A smaller Lamport timestamp is necessary for ancestry but insufficient to prove it.
• An unbounded causal buffer turns one lost dependency into memory exhaustion; fetch, timeout, and observability are required.
• Redelivery preserves causal context but must not reapply a non-idempotent business effect.

Boundaries and non-guarantees

• Happens-before is not consensus, linearizability, a global real-time clock, or a transport guarantee.
• A deterministic total order may hide rather than resolve concurrent conflicts.
• Dynamic membership changes causal-metadata identity and garbage-collection requirements.

Related material

Primary sources

1. Lamport, Time, Clocks, and the Ordering of Events in a Distributed System
2. Microsoft Research publication page for Time, Clocks, and Ordering Events
3. Mattern, Virtual Time and Global States of Distributed Systems