I wanted Jepsen's Elle in CI without a JVM, so I wrote adya

Your database documentation says REPEATABLE READ. Your code assumes it. Have you ever checked?

I spent the last stretch building adya, a black-box checker for transactional isolation. You give it a log of transactions a database ran, and it tells you which isolation guarantees held. For each one that didn't, it prints the transactions involved and the chain of reads and writes that proves the violation.

It's an independent Rust implementation of the approach from Elle (Kingsbury and Alvaro, VLDB 2020), the checker behind Jepsen's database analyses. If you know Elle, adya reads the same history formats and takes the same flags. If you don't, keep reading.

The problem with "it passed the tests"

Isolation bugs don't show up in unit tests. They need two or more transactions to interleave in one particular way, and when they happen nothing crashes. You just get a balance that's off, or two people booked into the same seat.

The classic example is write skew. Two doctors are on call, and the rule says at least one must stay on call. Each doctor's transaction checks "is the other one still on call?", sees yes, and takes themselves off. Both commit. Now nobody is on call.

Snapshot isolation allows this. Postgres's REPEATABLE READ is snapshot isolation, so it allows this. If you thought REPEATABLE READ meant "safe enough", the bug ships.

Elle's insight was that you can catch this from the outside. Record what every client asked for and what it got back, infer the dependencies between transactions, and look for cycles that a given isolation level forbids. Atul Adya's 1999 thesis catalogued those cycles (G0, G1c, G-single, G2 and so on), which is where the name comes from.

Why another implementation

Elle is excellent. It's also a Clojure library on the JVM. People who want it outside a Jepsen test end up shelling out to elle-cli from a Go or Python harness. I found two open-source projects doing exactly that in CI (barn, bytecaskdb), and the bytecaskdb PR lists what went wrong: a blocked Clojars mirror, a crash when graphviz was missing, log lines corrupting the JSON output.

On my Windows machine, elle-cli 0.1.11 hung with no output on every anomalous history I gave it. On Linux it worked, but in my CI comparison it needed more than five minutes on five of forty random 300-transaction histories, and ran out of a 6 GB heap on one more. adya checked all forty in 0.2 seconds.

Elle also leaves the workload to you. You have to write the client that generates transactions, runs them against your database and records the history. That's the part most people never get to.

So adya ships both halves in one binary:

cargo install adya

# Run a workload against Postgres at REPEATABLE READ,
# then check the history against serializability.
adya run postgres --url postgres://localhost/test -i repeatable-read -c serializable

What it looks like

You don't need a database to try it. adya has a built-in simulated database that implements isolation levels the textbook way:

$ adya run sim -i snapshot-isolation -c serializable -n 300 -p 4 --seed 1
history.jsonl   false

G2-item #0
  Let:
    T234 = {"index":234,"process":1,"type":"ok","value":[["r",10,[4]],["append",3,6],["r",3,[4,5,6]]]}
    T237 = {"index":237,"process":3,"type":"ok","value":[["append",9,13],["append",10,5],["r",3,[4,5]],["r",10,[4,5]]]}
  Then:
    - T234 < T237, because T234 did not observe T237's append of 5 to 10.
    - However, T237 < T234, because T237 did not observe T234's append of 6 to 3: a contradiction!

That's the doctors problem with list keys. T234 read key 10 before T237 appended to it, so T234 has to come first. T237 read key 3 before T234 appended to it, so T237 has to come first. Both can't be true, so no serial order exists. Snapshot isolation allows that cycle. Serializability doesn't.

How it works

The trick that makes this tractable is the workload. adya's default, borrowed from Elle, is list-append: every key holds a list, transactions append unique numbers to lists and read whole lists back. Each read then tells you the order of every append before it. If one client read [1, 2] and another read [1, 2, 5], you know 5 came after 2, without asking the database anything.

From those orders adya builds a dependency graph over transactions, using Adya's three edge types:

• ww: T2 appended right after T1's append to the same key.
• wr: T2 read a list ending in T1's append.
• rw: T1 read a list that T2 later appended to, so T1 didn't see T2's write.

If you're checking a model with real-time guarantees (strict serializability), it adds edges for "T1 finished before T2 started", using a transitive reduction so the graph stays roughly linear in the history.

Then it looks for cycles, one strongly connected component at a time. Each anomaly class is a cycle with constraints. G-single has exactly one rw edge. G2-item has at least two, with two of them adjacent. G1c has no rw edges and at least one wr. Instead of enumerating cycles and classifying them afterwards, adya runs a breadth-first search over pairs of (transaction, path state). The path state is seven bits: how many rw edges so far (0, 1, or 2+), whether the last edge was rw, whether the first one was, whether two were adjacent, whether it has seen a wr, and whether it has used a real-time edge. One BFS then returns the shortest cycle of exactly the shape you asked for.

Before searching, it runs cheaper existence checks. For each model it asks whether the subgraph that model forbids cycles in has a nontrivial SCC at all. If the ww/wr-plus-one-rw subgraph is acyclic, snapshot isolation holds as far as cycles go, and adya skips every search that could only find SI violations. It also searches the most severe anomalies first and skips anything they imply. A 100,000-transaction history (30 MB of JSON) checks in about 1.6 seconds on my laptop.

Is it right?

A checker that's wrong is worse than none, so this took most of the work.

1. Elle's own expected results. elle-cli's test suite ships 56 list-append and rw-register histories along with the JSON verdicts Elle produced for them. adya matches all 56: same verdict, same anomaly types, and the same weakest models ruled out. Getting there taught me two Elle details I would never have guessed. It labels an edge that carries several relations by a fixed priority (ww before wr before rw before real-time), but tests whether a cycle exists using any relation the edge carries. And it counts a composed edge that loops back to the same transaction as a cycle.
2. Elle itself, live. On every push, CI generates random histories with adya's simulator and checks each with both tools. In the first full run Elle finished 34 of 40, and adya agreed on all 34.
3. Databases with known answers. The simulator implements serializable, snapshot isolation, read committed (with write locks), read uncommitted, and a deliberately broken "snapshot" that writes back stale state. Tests assert that correct runs produce zero anomalies at their own level and the expected ones above it. That test caught a bug in my simulator, not in the checker: my first read committed took no write locks, which is weaker than any real database.

What Postgres and MySQL did

CI runs 4,000 transactions from 10 clients over 6 hot keys against Postgres 17 and MySQL 8.4, at each isolation level, and checks every history against a ladder of models. List-append results:

database, level	serializable	snapshot isolation	read committed
Postgres READ COMMITTED	G-single, G2-item, internal, lost update	G-single, internal, lost update	valid
Postgres REPEATABLE READ	G2-item	valid	valid
Postgres SERIALIZABLE	valid	valid	valid
MySQL REPEATABLE READ	G-single, G2-item, internal, lost update	G-single, internal, lost update	valid
MySQL SERIALIZABLE	valid	valid	valid

Postgres did what its docs say. REPEATABLE READ is snapshot isolation, write skew included, and SERIALIZABLE came out strict serializable. I also restarted Postgres every few seconds during a 6,000-transaction SERIALIZABLE run (--fault "docker restart -t 0 pg"). Nine restarts, 2,957 commits, 3,043 failures, and the history still checked clean.

MySQL's REPEATABLE READ is weaker than its name. It lets a transaction lose another's update and see part of another transaction's writes, so it isn't snapshot isolation. Jepsen reported the same thing about MySQL 8.0.34 in 2023. adya reproduces it from a cold start in a few seconds.

Testing your own database

The built-in drivers cover SQLite, Postgres and MySQL. For anything else there's adya run exec: adya starts your client once per process, writes one JSON line per transaction to its stdin, and reads back one line saying what happened.

{"value":[["append",3,7],["r",4,null]]}
{"type":"ok","value":[["append",3,7],["r",4,[1,7]]]}

The repo has a 59-line Python client for SQLite as a template. Swap the SQL and you're testing your own database.

Limits

adya covers list-append and read-write register workloads. It doesn't do predicate reads, or Elle's bank, set and counter checkers. It prints text proofs instead of Graphviz plots. A clean result means it found no anomaly in that history. It doesn't prove your database is correct, so run it longer, with fewer keys for more contention, and with faults.

If you run it against something interesting, I'd like to hear what it found. Issues and PRs are open.

• GitHub: https://github.com/zaydmulani09/adya
• crates.io: https://crates.io/crates/adya

Comments

[shieldx]

The gap between what a database documentation claims and how it actually behaves under concurrency is where most subtle bugs hide. I've seen entire distributed systems fail because someone assumed a specific isolation level was being strictly enforced by the engine, only to find out that certain edge cases or specific configurations defaulted to something much weaker. Moving these types of consistency checks into a lightweight CI pipeline without the JVM overhead is a massive win for developer velocity. It's much easier to iterate on testing strategies when you aren't fighting with heavy startup times or memory constraints every time you want to verify a transaction boundary.

[Zayd Mulani]

Thanks. That gap is exactly why I made it run the workload too, so you can point it at your own config instead of trusting the docs.