“Linearizable”, “serializable”, “no acknowledged write is lost” are properties of every history a system can produce, not of its happy path. The test that can refute such a claim has four parts: concurrent clients run a generated workload; a nemesis injects partitions, crashes, pauses and clock skew; every invocation and completion is recorded with its outcome; and a checker searches the recorded history for an ordering the specification allows. Example-based integration tests exercise the interleavings someone thought of; the bugs that matter here live in the others.
type regIn struct {
write bool
value int
}
type regOut struct {
value int
unknown bool // the client timed out: the write may or may not have happened
}
// The model is the specification: a single register, no replication, no faults.
var register = porcupine.Model{
Init: func() any { return 0 },
Step: func(state, in, out any) (bool, any) {
i, o := in.(regIn), out.(regOut)
if i.write {
return true, i.value
}
return o.value == state.(int), state
},
}
// A timed-out write is not a failed write. It stays open to the end of the
// history, so the checker may place its effect anywhere after the call — or
// after every other operation, which is the same as never.
func indeterminateWrite(client, value int, call int64) porcupine.Operation {
return porcupine.Operation{
ClientId: client, Input: regIn{write: true, value: value},
Call: call, Output: regOut{unknown: true}, Return: math.MaxInt64,
}
}
func checkHistory(t *testing.T, history []porcupine.Operation) {
res, info := porcupine.CheckOperationsVerbose(register, history, time.Minute)
switch res {
case porcupine.Illegal:
_ = porcupine.VisualizePath(register, info, "history.html")
t.Fatal("history is not linearizable; see history.html")
case porcupine.Unknown:
t.Fatal("checker timed out: partition the history by key or shorten it")
}
}What makes the verdict mean something. The oracle is a model of the contract, not the implementation’s own assertions: a sequential register or map for linearizability, a dependency graph for isolation. Linearizability is a local property — a history is linearizable iff each object’s sub-history is — which is why checkers split the history per key; checking it in general is NP-complete, so the workload is shaped for the checker (few keys, short per-key histories). Elle infers Adya’s dependency graph from transactions whose reads reveal version order (append to lists, read the whole list), which keeps isolation checking roughly linear in history length (90). Indeterminate operations: a timeout is neither success nor failure (24). Recording it as a failure makes a correct system look broken when the write later appears; dropping it entirely does the same; the only sound encoding is “may take effect at any point after the call” — the Return: math.MaxInt64 above. Safety versus liveness: every property is the intersection of a safety and a liveness property, and only the safety part has a finite witness. A finite history can prove a lost write; it can never prove that progress will not come. “The cluster recovers” is checked by healing every fault and demanding progress within a bound — a test of the bound, not a proof.
Two ways to drive the schedule. Black-box (Jepsen, etcd’s robustness suite): real binaries on real nodes, faults through the network and the process table. It tests what ships, and a failure found this way may never replay. Deterministic simulation (FoundationDB): network, disk, time and the random generator sit behind interfaces, the whole cluster runs as a discrete-event simulation in one thread, and a seed replays a run exactly; “buggification” makes rare code paths common, swarm testing randomises which faults and knobs each run enables, and simulated time skips idle stretches. The price is that it has to be designed in (54), and it cannot exercise code outside the simulator or a dependency whose real contract is weaker than believed — FoundationDB’s own paper names both limits. Neither is chaos engineering (77): a chaos experiment asks whether an aggregate steady-state metric survives a fault; this asks whether a single history breaks the contract. A green chaos run says nothing about a lost write. And neither is model checking (99), which covers every schedule of a small model of the design; these tests sample schedules of the real implementation.
Decision rule. A consistency level written into an API contract (65) gets a history checker for that level in CI, run under a nemesis; a vendor’s level is a hypothesis of the same kind — the Elle paper opens by noting that many databases do not provide the isolation they claim. Every anomaly found is kept as a minimal history and replayed as a regression test. A run that finds nothing bounds nothing: its strength is exactly the faults, workload and duration it covered, so report those next to the green result.