Time, causality & histories
An order written in a log is useful only after you say which relationships it must preserve.
Who could know what?
Select two events and trace their causal path.
Loading activity… Enable JavaScript to interact; the course text remains readable.
Runs in your browser with synthetic state. This is not a live etcd cluster. Read the concept · Inspect real evidence
Learning goals
Build a happens-before relation, distinguish logical time from wall time, and translate a request trace into operation intervals.
Prerequisites: system and failure assumptions.
Causality is a partial order
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.
Operation histories have two boundaries
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.
Hands-on: read the intervals
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.
Self-check
Does L(a) < L(b) mean a caused b?
No. Logical clocks preserve causal order in one direction. Two independent events can also have different Lamport timestamps.
Can a timed-out write be deleted from a correctness history?
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.
Read the originals
- Lamport — Time, Clocks, and the Ordering of Events in a Distributed System, causal order and logical clocks.
- Herlihy & Wing — Linearizability, operation histories and real-time constraints.
Study alongside MIT 6.5840
Lecture 8: Consistency and Linearizability
Trace a transitive causal path and a concurrent pair; logical-clock supplement is Lamport 1978, not a dedicated MIT lecture claim.
node tests/demo-models.test.mjsOur runnable exercise is an independent original, not the linked MIT assignment solution. Setup is on the reproduce page; no enrollment, grade or certification is implied.
Search the verified course map →