Which checker checks which isolation level

The paper that fixed the complexity landscape. Six levels defined axiomatically over the write-read relation plus a commit order; RC, RA and CC are decided by saturation in polynomial time, while PC, SI and SER are NP-complete and fall to polynomial only when history width is fixed — or, more generally, when the biconnected components of the communication graph are bounded. Found violations in CockroachDB, Galera and AntidoteDB.

Deliberately trades completeness for speed: it infers an Adya dependency graph directly from observed values and detects cycles, so it is linear-to-log-linear in history length and near-independent of concurrency, but may miss anomalies. Coverage is expressed as Adya anomaly classes (G0, G1a/b/c, G-single, G2) which the library maps onto named models. The list-append datatype is what makes it work — appends are traceable, so each version has one trace and write-write order is recoverable. With no predicate support it cannot separate repeatable read from serializability.

Serializability only, and the non-strict variant deliberately — the harder problem. Encodes the history as a polygraph, prunes impossible constraint choices with GPU-accelerated transitive closure, then decides acyclicity in MonoSAT. The encoding is provably equivalent to the existence of an acyclic serialization graph, so the gap is termination time, not missed anomalies. Periodic fence transactions make epoch-based garbage collection safe, which is what allows continuous checking at ~2K txn/s.

Cobra's approach retargeted at SI. The generalized polygraph compacts the uncertain dependencies inherent to black-box observation into one structure; reachability pruning then SAT/MonoSAT decides it, and a recovery pass turns the counterexample into a readable anomaly. Complete for histories of determinate transactions. Scales to a billion keys and a million transactions in under four hours; reproduced all 2,477 known SI anomalies and found new ones in Dgraph, MariaDB-Galera and YugabyteDB.

Introduces the BC-polygraph, adding begin/commit constraint edges so that acyclicity is exactly SI. Sound and complete for Adya SI; the real-time variants (generalized SI, strong SI) need wall-clock timestamps with a bounded-drift assumption, and if drift exceeds it Viper may reject an SI history. Notable among this group for handling range queries via tombstones — deletes become markers carrying write IDs.

A test suite rather than a decision procedure, and the only entry here with no formal soundness or completeness claim. It collects interval-timestamped client traces and replays them through a local mirror of DBMS concurrency-control machinery — lock tables, version chains — applying four abstracted checks (consistent read, mutual exclusion, first-updater-wins, serialization certifier) instead of cycle detection. Designed for sharded, pipelined, garbage-collected operation on long runs. 24 bugs reported in commercial DBMSs; Vbox's comparison scores its anomaly coverage low, so treat it as a bug-finder.

Not black-box, and that is the whole idea. Version certificate recovery pulls the expected version order out of the DBMS — Debezium CDC on Postgres, CHANGEFEED on CockroachDB, heap scans on TiDB — which removes the search for a version order and, uniquely in this survey, makes predicate dependencies tractable (O(P·W)). Soundness is conditional on the certificate being right. The TOCS extension adds Enne, which replays in an expected serialization order for a further 34–430× over Emme, and King Cobra, a version-order-informed Cobra.

The first sound and complete checker for the HAT family. Its contribution is a set of 14 transactional anomalous patterns with the theorem that a history satisfies a level exactly when it contains no instance of that level's patterns — so checking is graph construction plus pattern matching, no solver. Vector-clock reachability with tree clocks gives O(1) amortized clock operations. Catches things the strong-isolation checkers structurally miss: intra-transactional anomalies, future reads, monotonic-read violations.

Not a new algorithm — an integration platform that wraps sound-and-complete checkers for six levels behind one interface over MySQL, PostgreSQL and MariaDB, with counterexample visualization (the core transactions and their dependencies drawn out) and CPU/memory benchmarking. Useful as the practical front-end for the Nanjing/ETH line of checkers.

Closes the complexity question at the weak end. Builds a minimal saturated partial commit relation and checks acyclicity: Θ(n^3/2) for RC and RA — matching conditional lower bounds under the combinatorial BMM hypothesis — and O(n·k) for CC, dropping to linear when transactions are O(1)-sized. Sessions barely help: RA keeps the n^3/2 bound with just two sessions. Against Plume it is a mean 245× (RC), 193× (RA), 62× (CC) on large histories — polynomial degree ~6 down to 1.5.

Buys its way out of NP-hardness by asking the database for start and commit timestamps. Those directly give the arbitration and visibility relations, so there is no polygraph to search — correctness reduces to checking the SESSION, INT, EXT and NOCONFLICT axioms incrementally. Chronos is offline at O(N log N + M); Aion is online, amortized O(log N + M) per transaction, sustaining ~12K txn/s alongside a live system. Grey-box, not black-box.

Restricts the workload instead of the algorithm. A mini-transaction is a read-modify-write with at most four operations; under that restriction checking collapses out of NP-hardness — O(n) for SER and SI, O(n²) for SSER. Sound and complete for MT histories, so it is a bug-finding guarantee rather than a general decision procedure. ~1600× over PolySI on SI under Zipfian keys, ~5× over GPU-Cobra on SER.

Extends the Cobra framework with predicate constraints and client-side timestamps for time-dependency inference, plus incremental reachability (Purdom + Italiano) so transitive closure costs O(|V| + |E∖T|) rather than O(|V|³). Reports 60–100× over Cobra with 20–70× less memory at 10K transactions, and constraint counts cut from ~500K to a few tens of thousands. Claims 13/13 read-after-transaction anomalies against Cobra's 6/13.

The current state of the art on the NP-hard side, and the one that drops the unique-value assumption that Cobra, PolySI, Viper and Elle all require — so it applies to general workloads with duplicate written values. Hyper-polygraphs represent certain and uncertain dependencies together; small-width cycle preprocessing and order-guided polarity picking from a pseudo-topological order tune the SMT search. Up to 4.4× over GPU-Cobra and 4× over PolySI, at 100K transactions / 2M operations.