adya

Transaction isolation, implemented and convicted. An MVCC engine with four isolation levels — including Cahill's SSI — and a dependency-graph checker that finds G0, G1a, G1b, G1c, G-single and G2-item in observed histories.

Named for Atul Adya, whose 1999 thesis replaced the ANSI standard's prose definitions of isolation levels with the phenomena this repository implements and detects.

Every database advertises isolation levels. Almost nobody can show you what theirs actually admits.

The claim "we provide snapshot isolation" is really two claims — that nothing weaker than SI ever happens, and that SI is genuinely what you get rather than something stricter wearing the name — and neither is checkable by reading the code. They are properties of executions, so you have to catch executions and interrogate them.

The ladder

read-uncommitted     sound over 150 schedules   admits G1b at seed 0
read-committed       sound over 150 schedules   admits G-single at seed 1
snapshot-isolation   sound over 150 schedules   admits G2-item at seed 25
serializable         sound over 150 schedules   admits nothing, commits 51%

Each rung is held to two things:

Sound — over hundreds of seeded schedules, the engine at level L never produces an anomaly L is required to prevent.

Weak — there exists a schedule where it does produce the anomaly the next rung prevents. So L sits exactly where the literature puts it, rather than being a stricter level under a weaker name.

The second direction is the one that matters. Soundness alone proves almost nothing: an engine that aborted every transaction would be sound at every level, and a checker that found nothing would agree with it. Requiring each rung to exhibit the next rung's forbidden phenomenon closes that hole — and it checks the checker, because a checker that could not find write skew under snapshot isolation would have nothing behind its acquittal of serializable either.

Neither side is trusted alone. Each convicts the other.

The last line matters too. serializable commits 51% of its transactions under a contended workload; an acquittal bought by aborting everything would be worthless, so the commit rate is asserted, not just reported.

Checked against a database somebody else wrote

Everything below this section checks my engine with my checker. That is clean and completely closed: if both sides shared a misunderstanding, nothing here would notice.

So the checker is pointed at PostgreSQL 18, whose behaviour is documented independently and whose answers are known before the run starts. Its REPEATABLE READ is snapshot isolation — the manual says so, and says write skew is possible there. Its SERIALIZABLE implements Cahill, Röhm and Fekete's SSI, the same algorithm mvcc.ts implements.

The directed write-skew scenario. Two transactions, each reading what the other is about to write:

| PostgreSQL level | Outcome | Checker's verdict | | --- | --- | --- | | READ COMMITTED | both commit | G2-item T2 —rw→ T1 —rw→ T2 | | REPEATABLE READ | both commit | G2-item — clean as snapshot isolation, violation as serializable | | SERIALIZABLE | one aborted | nothing |

A random sweep, 25 rounds of three concurrent transactions each:

| PostgreSQL level | Aborts | Anomalies found | | --- | --- | --- | | READ COMMITTED | 0 / 100 | G-single × 24 | | REPEATABLE READ | 32 / 100 | none | | SERIALIZABLE | 32 / 100 | none |

Read that table against the ladder further down and it is the same shape. Read committed admits read skew and never aborts for isolation's sake. Repeatable read prevents read skew and pays for it in aborts, while still permitting write skew when the scenario is built for it. Serializable admits nothing and pays the same price.

PostgreSQL reproduces the ladder, and it did not consult this repository to do so. That is the point: the checker got a known answer right, in both directions, on a system that does not care what I think — and anyone with a Postgres can run against-postgres/ and see the same thing.

npm run test:postgres     # ADYA_PG=postgres://... to point elsewhere

What the phenomena are

From Adya §3, and used here by their own names so a reader can check this against the source rather than against my paraphrase.

| | | | --- | --- | | G0 | a cycle of write-dependencies alone | | G1a | a read of a value written by a transaction that then aborted | | G1b | a read of a value its writer replaced later in the same transaction | | G1c | a cycle of write- and read-dependencies | | G-single | a cycle containing exactly one anti-dependency — read skew | | G2-item | a cycle containing more than one — write skew |

Each level forbids everything the level below it forbids, plus one more:

| Level | Adds | | --- | --- | | read uncommitted | G0 | | read committed | G1a, G1b, G1c | | snapshot isolation | G-single | | serializable | G2-item |

The distinction between the last two rungs is one anti-dependency. Read skew has one and snapshot isolation prevents it; write skew has two and snapshot isolation cannot. That gap is the entire practical difference between SI and serializability, and getting a checker to tell them apart is most of the work in check/.

How the checker can know

To draw a write-dependency edge you must know which write came first — and from an execution over ordinary registers you cannot. Two writes of the value 5 leave the same trace, so the version order is unrecoverable and the graph cannot be built.

So keys hold append-only lists, and every append writes a globally unique element. Now a single read of [a, b, c] states, by itself, that a preceded b preceded c. The version order is recovered from the observations rather than taken from the store's internals — which is what keeps the checker independent of the thing it checks. An engine that lied about its own ordering would be caught rather than believed.

That idea is the core of Elle (Kingsbury & Alvaro, VLDB 2020) and this borrows it wholesale.

With the version order in hand, the graph follows: ww between consecutive versions, wr from a writer to whoever read it, rw from a reader to whoever wrote the version it missed. Then Tarjan finds the strongly connected components, and a breadth-first search inside each finds the shortest cycle — because "there is a cycle among these forty-one transactions" is not a bug report, and two transactions with their edges spelled out is.

Each phenomenon gets its own targeted search rather than one cycle hunt and a shrug, since a single component can contain cycles of several classes at once and reporting whichever came first would understate the problem.

How the engine differs by level

One engine, four rungs, and what changes is small — which is the point. The difference between snapshot isolation and serializability is not a different database, it is one extra check.

read-uncommitted     reads see other transactions' buffered writes
read-committed       reads see the latest committed version, each time
snapshot-isolation   reads see the snapshot at start; first committer wins
serializable         the above, plus Cahill's SSI

Appends are read-modify-write on the key's value, as SET v = v || 'x' would be. That is what makes two concurrent appends to one key a real write-write conflict rather than two commuting operations — without it, first-committer-wins has nothing to do and write skew is not expressible.

SSI follows Cahill, Röhm and Fekete (SIGMOD 2008), the algorithm PostgreSQL implements. Snapshot isolation's remaining hole has a shape: any cycle it admits contains two consecutive anti-dependency edges. So it is enough to watch for a transaction with both an incoming and an outgoing one — the pivot — and refuse to let it commit. The check is deliberately conservative: it aborts some transactions that would have been serializable anyway, which costs throughput and never costs correctness.

Usage

npm install @botiroff/adya

Or to work on it:

npm install
npm test        # engine and checker
npm run museum  # the ladder

import { Store, checkHistory } from "@botiroff/adya";

const store = new Store();
store.begin("t1", "serializable");
store.read("t1", "x");
store.append("t1", "y");
store.commit("t1");

const report = checkHistory(store.history, "serializable");
// { ok: true, violations: [], observed: [], stats: { ... } }

The checker takes any history in its format, so it is not tied to this engine. Point it at a real database's history and it will answer the same question.

Limits

No predicate anti-dependencies. Plain G2 needs predicate reads — SELECT ... WHERE. This workload has none, so there is nothing to infer them from, and claiming to check for them would be claiming more than the evidence supports. Only G2-item is checked.

Aborts instead of blocking. Real engines block on a write conflict and detect deadlock; this refuses the write. That lets fewer interleavings commit, and admits no history that blocking would not.

Not a database. No durability, no recovery, no indexes, no predicates, no garbage collection of old versions. It is an isolation engine and nothing else.

Passing is not proof. Hundreds of seeds is hundreds of schedules from an astronomically larger space. It is a very good fuzz run, not a theorem.

For the smallest instance the theorem is available: pnueli model-checks the textbook write-skew scenario exhaustively. Under snapshot isolation the constraint is reachably false in five steps; with a rule that aborts a transaction whose snapshot has been overtaken it is unreachable across every state the model can produce. That is the same fact this repository finds at seed 25 of 300, stated without the seed.

The checker is sound, not complete, on cycles it reports as shortest. It finds a shortest cycle through each component member, which is the shortest overall for the components these workloads produce, but exhaustive enumeration of every cycle is not attempted.

Prior art

The phenomena and their numbering are Adya's thesis (MIT, 1999), which formalised what Berenson et al. had shown was wrong with the ANSI SQL definitions in 1995. Serializable snapshot isolation is Cahill, Röhm and Fekete (SIGMOD 2008). The list-append trick that makes version order recoverable is Elle (Kingsbury & Alvaro, VLDB 2020), the checker Jepsen uses to find these anomalies in real databases.

Schedules are made reproducible by unflake.

Who wrote this

Doniyor Botirov, founder of dbit.one. The reasoning behind this repository at length — what each isolation level actually admits, and why write skew is the expensive one: Isolation levels: what your database actually admits.

License

MIT