An order written in a log is useful only after you say which relationships it must preserve.
Build a happens-before relation, distinguish logical time from wall time, and translate a request trace into operation intervals.
Prerequisites: system and failure assumptions.
Within one process, earlier steps precede later steps. Sending a message precedes receiving that message. Taking the transitive closure gives happens-before. If neither event reaches the other through these edges, they are concurrent in this model—even if their wall-clock labels differ.
A: a1 ── send(m) ───────────────── a3
╲
B: b1 ───────── receive(m) ──────── b3
C: c1 ──────────────────────────── c2
No message edges to C: timestamps alone add no causality.A Lamport clock increments on local events and advances beyond the received timestamp on message receipt. If a → b, then L(a) < L(b). The converse does not hold: a smaller counter does not prove causality. Breaking ties with process IDs creates a convenient total order but does not discover missing causal edges. Vector clocks can retain more causal information at a metadata cost; this first edition does not implement them.
A client's invocation and response delimit an operation. The server's commit event is usually inside that interval for a successful call, but the client does not observe it directly. A timed-out call can continue beyond the client's waiting interval. Do not turn the deadline into a successful-operation response in a checker.
| Record | What it supports | What it cannot establish alone |
|---|---|---|
| Client monotonic start/end | Intervals on one recorder's clock | A global order across unsynchronized hosts |
| Server revision | Order of mutations in that etcd cluster lineage | UTC time or cross-cluster order |
| Timeout | No successful response by a deadline | No side effect |
Our real runs use one host and one orchestrator. Duration measurements use its monotonic clock. The saved JSON is selected mechanism evidence, not a packet capture. Our interactive checker accepts only completed reads/writes with finite intervals supplied on a comparable time axis.
Open the history workbench. Load “Concurrent.” The write spans 0–4; the first read spans 1–3 and returns the initial value 0. A legal explanation puts that read before the write. The next read, starting at 5, must reflect the completed write if the model is linearizable.
w1: write(1) [0,4]
r1: read()→0 [1,3]
r2: read()→1 [5,7]
possible order: r1 → w1 → r2Move r1.start to 4.5 and r1.end to 4.8. Run again. The real-time edge now forces the write before that stale read, so no legal register order remains.
No. Logical clocks preserve causal order in one direction. Two independent events can also have different Lamport timestamps.
Not generally. It might have taken effect. A complete checker must reason about possible completions or omission of pending operations. This workbench rejects pending operations and makes no claim about such histories.