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.

Related material

Primary sources

1. Jepsen repository and framework README
2. Jepsen checker API documentation
3. Knossos linearizability checker
4. Elle transactional anomaly checker
5. Jepsen MongoDB 4.2.6 analysis