Lamport Clocks and Happens-Before Reasoning

Learning outcomes

AtlasMart now needs an ordering marker that survives wall-clock skew. The goal is not to know “what time it really was,” but to ensure that if one event could have influenced another, the second event receives a greater logical timestamp. Lamport's clock construction does exactly that with one integer per process and a simple rule on message receipt.

1. Happens-before is a partial order

Lamport writes the relation as an event a “happened before” event b when at least one of three conditions holds: they occur in the same process and a precedes b; a is the send of a message and b is its receipt; or the relation follows transitively through other events. If neither a → b nor b → a is established, the events are concurrent with respect to this model.

This is a partial order because some pairs have no causal relation. That is not missing data to be guessed from wall-clock timestamps. It is a meaningful statement: the system has no message/program-order evidence that either event influenced the other.

2. Lamport's logical-clock rules

If clocks obey these rules, then a → b implies C(a) < C(b). This is the key guarantee. The number is a logical marker; units such as milliseconds are meaningless.

3. Trace one AtlasMart order through two nodes

Node A records a local event, then sends an order. Node B receives it and reserves stock. The receive rule forces B's clock beyond the send timestamp even if B had processed fewer local events before the message. A third node C edits profile preferences without any communication path to A or B.

A: A1 local [L=1] -> A2 send order [L=2] ----message---->
B:                                             B1 receive [L=3] -> B2 reserve [L=4]
C: C1 profile [L=1] -> C2 preferences [L=2]

Known: A2 -> B1 -> B2
Unknown: B2 vs C2 (no causal path)

4. The clock condition is one-way

The common mistake is to invert the theorem. From C(a) < C(b) you cannot conclude a → b. Independent processes increment their own counters, so concurrent events can receive different logical values. Even equal values on two different nodes do not imply they are the same event.

A system can extend Lamport timestamps to a deterministic total order with a tie-breaker such as (logical_timestamp, node_id). That can be useful for replay, logs, lock queues, or deterministic conflict resolution. But the tie-breaker manufactures order between concurrent events; it does not discover a hidden causal relation.

5. Deliberately wrong approach — reject every smaller Lamport timestamp as “older causally”

Imagine AtlasMart receives two independent profile edits: one from node B at logical time 4 and one from node C at logical time 2. A naive merge keeps only B because 4 is greater. Nothing in the clock says B observed C or superseded it. The rule silently converts an arbitrary counter order into conflict semantics.

The repair is to choose metadata appropriate to the question. If you only need an order compatible with causality, Lamport clocks are sufficient. If you need to determine whether one version descended from another or whether two versions are concurrent, a vector-style causal context can encode more information.

6. AtlasMart lab — implement Lamport clocks

from dataclasses import dataclass

@dataclass
class Node:
    name: str
    clock: int = 0

    def local(self, label):
        self.clock += 1
        return (label, self.name, self.clock)

    def send(self, label):
        self.clock += 1
        return (label, self.name, self.clock)

    def receive(self, label, remote_clock):
        self.clock = max(self.clock, remote_clock) + 1
        return (label, self.name, self.clock)

A, B, C = Node("A"), Node("B"), Node("C")

history = []
history.append(A.local("A1 local"))
msg = A.send("A2 send order")
history.append(msg)
history.append(B.receive("B1 receive order", msg[2]))
history.append(B.local("B2 reserve stock"))
history.append(C.local("C1 independent profile edit"))
history.append(C.local("C2 independent preference edit"))

print("Lamport timestamps")
for label, node, ts in history:
    print(f"{label:31} node={node} L={ts}")

print("\ncausal chain:")
print("A2 send order -> B1 receive order -> B2 reserve stock")
print("timestamps:", msg[2], "<", history[2][2], "<", history[3][2])

print("\nconcurrency warning:")
print("B2 has L=", history[3][2], "and C2 has L=", history[5][2])
print("numeric order exists, but there is no message path proving B2 happened-before C2 or vice versa")

total_order = sorted(history, key=lambda x: (x[2], x[1]))
print("\ndeterministic total order using (Lamport, node-id):")
for x in total_order:
    print(x)
print("this tie-broken total order is useful for deterministic ordering, not proof of causality")

Expected output

Lamport timestamps
A1 local                        node=A L=1
A2 send order                   node=A L=2
B1 receive order                node=B L=3
B2 reserve stock                node=B L=4
C1 independent profile edit     node=C L=1
C2 independent preference edit  node=C L=2

causal chain:
A2 send order -> B1 receive order -> B2 reserve stock
timestamps: 2 < 3 < 4

concurrency warning:
B2 has L= 4 and C2 has L= 2
numeric order exists, but there is no message path proving B2 happened-before C2 or vice versa

deterministic total order using (Lamport, node-id):
('A1 local', 'A', 1)
('C1 independent profile edit', 'C', 1)
('A2 send order', 'A', 2)
('C2 independent preference edit', 'C', 2)
('B1 receive order', 'B', 3)
('B2 reserve stock', 'B', 4)
this tie-broken total order is useful for deterministic ordering, not proof of causality

The trace verifies the clock condition on the message chain. It also prints a deterministic total order that includes C's independent events. That last list is useful only because the code declares a tie-break rule; it must not be read as a causal proof.

Verification checklist

• Every local/send event increments its node clock.
• B's receive timestamp is greater than A's send timestamp.
• The printed causal chain has strictly increasing logical values.
• The lesson explicitly marks B2 and C2 as causally unproven/concurrent despite their numeric ordering.
• No wall-clock API is needed.

7. Production judgment and next bridge

Lamport clocks are compact and powerful when the requirement is causal-compatible ordering: “receives must sort after sends,” “state-machine metadata must advance,” or “events need a deterministic tie-broken order.” They do not solve clock synchronization, external real-time ordering, bounded staleness, or concurrent-version detection.

Lesson 3 makes the tradeoff explicit. Version vectors carry one logical counter per actor/replica identity. The additional metadata lets two versions be compared component-wise, so the system can distinguish ancestor, descendant, equal, and concurrent states.

Authoritative references

• Lamport — Time, Clocks, and the Ordering of Events in a Distributed System — original definition of happens-before and logical clocks
• Kulkarni et al. — Logical Physical Clocks / Hybrid Logical Clocks — later work contrasting logical and physical time and motivating HLCs