Skip to content

Consistency History Checker

Verification audit — instantiates Shared-State Consistency Contract Design

Records the real interleaving of operations a system produced and mechanically checks whether that history is admissible under the claimed consistency model.

A Consistency History Checker takes an actual execution — the logged sequence of client operations, their arguments, return values, and timings — and asks a precise question: could a system that honestly provides the claimed guarantee have produced this history? Its distinguishing contribution is that it tests behavior, not labels: it does not trust that a store called "linearizable" is linearizable; it searches for a legal ordering of the recorded operations consistent with the model and, finding none, produces a concrete counterexample. It converts a consistency claim from a marketing word into a falsifiable property checked against evidence.

Example

A team about to ship a distributed message queue wants to know it really delivers each message to exactly one consumer, in the order it advertises, even under faults. They run a workload of concurrent enqueue and dequeue operations while injecting network partitions and node restarts, recording every operation with its start and end time. The checker then searches for a single ordering of the operations consistent with the queue's specification — each enqueued item dequeued exactly once, in an order a correct concurrent queue could have produced. It finds none: during a partition, message M-417 was handed to two different consumers. The output is not a vague "seems flaky" but a minimal history — these operations, in this interleaving, that no correct queue could produce. That one counterexample is worth more than a thousand passing runs.

How it works

The distinctive thing is that it is a decision procedure over recorded histories, not a live guard. It needs a machine-readable model — the sequential spec plus the ordering rule (linearizable, sequential, causal, serializable) — and a faithfully timestamped log. It then searches the space of admissible orderings; because linearizability checking is NP-hard in general, real checkers exploit structure (for example, analyzing the dependency graph of reads and writes for cycles, as serializability checkers do). A failure yields a counterexample; a pass means no violation was found in this run, never a proof of correctness.

Tuning parameters

  • Target model — linearizable / sequential / causal / serializable; the checker is only as meaningful as the model it checks against, and stricter models catch more but demand more from the log.
  • History length vs. tractability — longer runs surface rarer bugs but explode the search; windowing or dependency-graph methods trade completeness for feasibility.
  • Fault-injection pairing — whether histories are gathered under induced partitions and clock skew; anomalies mostly hide behind faults, so unfaulted runs rarely falsify anything.
  • Timestamp fidelity — how precisely operation start and end are captured; sloppy timing either masks real violations or invents false ones.

When it helps, and when it misleads

Its strength is being the only mechanism here that can disprove a consistency claim, turning "we think it's consistent" into a concrete counterexample engineers can debug — a single found violation is decisive. Its fundamental limit is the limit of all testing: absence of a counterexample is not proof — it validates the runs it saw, not the system. The classic misuse is running it on easy, unfaulted workloads, getting green, and reporting "verified linearizable" when the anomalies live precisely in the fault space that was never exercised.[1] The discipline is to pair it with aggressive fault injection, check against the actually claimed model, and read a pass as "not yet falsified," not "correct."

How it implements the components

  • consistency_violation_oracle — the checker is the oracle: the decision procedure that labels a recorded history admissible or not under the model.
  • audit_trail — it operates on (and often materializes) the durable, timestamped log of operations a history check requires and that later forensics reuse.

It judges histories but does not produce the guarantee it judges — the contract it checks against is Consistency Contract Decision Record's, the faults that make violations appear are Partition and Clock Fault Injection's, and live health signals are Replica-Lag and Freshness Dashboard's.

References

[1] Linearizability (Herlihy & Wing) — a history is linearizable if its operations can be placed in one total order that respects real-time precedence and each object's sequential spec. Checking it from a recorded log is the basis of tools such as Jepsen and Elle; such checking can refute a consistency claim but can only ever certify the observed runs, never the system. ↩