History checking: testing a consistency promise

How do you test whether a system keeps the consistency it promises, and what can a passing check prove?

"Serializable", "linearizable" and "snapshot isolation" are promises about every history a system may produce: which orderings of concurrent operations a reader may ever observe. You cannot measure such a promise the way you measure latency, because no single observation shows it. What you can do is record what actually happened under stress and search the record for something the promise forbids.

The method

1. Run a workload whose results reveal order. Many concurrent clients issue small operations chosen so that their outcomes expose the order in which they took effect: each write carries a unique value, or appends to a list whose later reads show every earlier append. A workload of ordinary reads and overwrites hides the order and leaves the checker guessing.
2. Inject the faults the promise must survive while the workload runs: partitions, crashed and restarted nodes, paused processes, clock skew. A history taken on a healthy cluster tests the easy case.
3. Record every operation as an interval: when the client invoked it, when the reply came back, and what it returned. An operation that timed out is recorded as unknown, not as failed, because a lost reply says nothing about whether the write happened (why a missing reply tells you nothing). The checker must then accept either outcome.
4. Search the history for a forbidden shape. For linearizability, every operation must appear to take effect at one instant between its invocation and its reply. For serializability, there must be one order of transactions that explains every value read. In practice the checker infers the dependencies between operations and looks for a cycle; each kind of cycle is a named anomaly (what the checker looks for).

The workload design in step 1 is what keeps step 4 affordable. Searching all orderings of a history is exponential in general. When the values themselves reveal the order, the search becomes building a graph and looking for cycles.

What a check can and cannot prove

The two outcomes are not symmetric.

• A found anomaly is a proof. The checker hands you a concrete history the promise forbids, with the operations that form the cycle. Nothing more is needed to show the claim is false for that configuration.
• A clean run proves almost nothing general. It shows that this history, under these faults, at this concurrency, admitted a legal order. Coverage grows with run length, concurrency and the variety of faults, but it never becomes a proof. This is the same boundary as chaos testing: you find only what your workload and your faults exercised.

So a history check belongs in the same frame as every other measurement here: state the promise as a hypothesis before the run, name the faults and the workload as the configuration, and report a clean result with its scope ("no anomaly in 2 hours at 50 clients under partitions and process pauses"), never as "the system is serializable".