System Design Cases
Jepsen Testing
Jepsen Testing — fault injection framework by Kyle Kingsbury for verifying claimed consistency guarantees of distributed databases. Shows Jepsen control node (op generator, nemesis fault injector, history recorder, Knossos/Elle checker) connected to a 5-node system-under-test. Three scenarios: setup with concurrent ops, partition-induced lost write, Knossos finding non-linearizable history. References real findings: MongoDB lost writes, Redis Sentinel split-brain, Cassandra LWT, Etcd recovery bug.
Jepsen testing: faults plus model checking over observed histories
Jepsen is black-box experimental testing: generators issue concurrent operations through real clients, nemeses inject selected faults, the harness records invocation/completion histories, and checkers compare those histories with explicit models. Knossos checks linearizability of suitable objects; Elle derives transactional dependency cycles and anomalies from carefully designed workloads.
A passing run is scoped evidence for that client configuration, workload, model, fault schedule, duration, and checker. It is not a proof of all executions. A timed-out operation is normally unknown because it may have committed; erasing that ambiguity can make an invalid history look valid.
Prerequisites and model
- Every logical operation has a stable id and invocation/completion record.
- The client preserves timeout/unknown outcomes and does not silently retry under a new identity.
- The workload exposes the property being checked; the checker has a correct sequential or transactional model.
- Nemesis lifecycle includes fault recovery and a quiescent observation period where relevant.
Correctness claims and invariants
- JEP-C1. Jepsen combines workload generation, real clients, fault injection, history recording, and formal checkers.
- JEP-C2. A linearizability checker requires an explicit sequential object model and invocation/completion history.
- JEP-C3. Elle detects transactional anomalies through dependency analysis for workloads designed to expose them.
- JEP-C4. Timeout operations retain unknown/possibly committed status rather than being discarded as failed.
- JEP-C5. A nemesis without a model checker is fault injection, not a Jepsen correctness conclusion.
- JEP-C6. No anomaly found is scoped evidence, not a proof for all workloads, faults, clients, or versions.
What the scenarios prove
- Model-history-checker pipeline (
pipeline): The runner generates operations and faults, records exact outcomes, then checks a declared model.
- Partition exposes stale read (
partition-stale-read): The nemesis isolates replicas while a register workload records a completed write followed by stale read.
- Timeout remains unknown (
timeout-unknown): A lost response may hide a committed operation, so the history records info/unknown.
- Knossos register check (
knossos-register): Knossos searches for a legal sequential register execution respecting real time.
- Elle transactional cycle (
elle-cycle): A transaction workload exposes dependency edges and an anomaly cycle.
- Passing run has scoped confidence (
scoped-confidence): No anomaly found is reported with workload, faults, checker, client, version, and duration.
Failure, concurrency, and retry traps
- Client defaults may weaken consistency unless configured and reported.
- Automatic retries can hide the original unknown operation and duplicate effects.
- A stale-read workload cannot validate multi-key serializability.
- Long histories can make general checkers intractable; partitioning by independent key is sound only when the property is local.
- Checker unknown/crash/resource exhaustion is not a valid pass.
Boundaries and non-guarantees
- Jepsen primarily tests observed safety; availability and latency need explicit metrics and thresholds.
- Clock-skew faults matter only when the system claim depends on clocks.
- A test cannot cover an undocumented membership or failover mode it never generates.
- Results apply to the exact software/client/configuration under test.