adya

A black-box checker for transactional isolation. Point it at a history of transactions your database executed and it tells you which isolation guarantees the database actually kept, with a step-by-step proof for every violation it finds: G0, G1a/b/c, G-single, G-nonadjacent, G2, lost update, and their process and real-time variants.

adya is an independent Rust implementation of the approach behind Jepsen's Elle (Kingsbury & Alvaro, VLDB 2020). It ships as one native binary with no JVM, reads the same history formats, and includes the half Elle leaves to you: a workload runner for SQLite, Postgres, MySQL, or any database you can drive from a subprocess.

$ 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!
...
Not repeatable-read.

That is write skew: each transaction read a key the other was about to change, which snapshot isolation permits and serializability forbids. adya found it from the outside, from nothing but what clients wrote and read; the same check runs against Postgres, MySQL, SQLite or anything else.

Why

Elle is the state of the art for finding isolation bugs; it has found violations in dozens of databases. But using it outside a Jepsen test means a JVM in your CI, a Clojure toolchain or elle-cli, and writing your own workload driver. Projects that want it end up shelling out to a JVM from a Go or Python harness (barn, bytecaskdb), and run into blocked Clojars mirrors, graphviz crashes, and logs interleaved into the JSON output. On the Windows machine where adya was written, elle-cli 0.1.11 hung, with no output, on each anomalous history it was given.

adya is the same idea in a form you can drop into any pipeline:

• one static binary (cargo install adya), or a Rust library;
• reads Elle's formats: elle-cli JSON, JSON lines, and Jepsen's history.edn, with elle-cli compatible flags (-m, -c, -a, --cycle-search-timeout);
• runs the workload too: adya run drives SQLite, Postgres or MySQL with concurrent clients, records an Elle-format history, and checks it;
• speaks to anything through adya run exec, a one-line-per-transaction JSON protocol your database client can implement in any language;
• fast: a 100,000-transaction history (200k operations, 30 MB) checks in about 1.6 seconds on a laptop.

Install

cargo install adya

Or build from source with cargo build --release. The database drivers are default features (sqlite, postgres, mysql); --no-default-features builds just the checker.

Try it in ten seconds

The built-in simulated database implements isolation levels the textbook way, so you can watch adya separate them without installing anything:

# Snapshot isolation permits write skew; serializability does not.
adya run sim -i snapshot-isolation -c snapshot-isolation   # valid
adya run sim -i snapshot-isolation -c serializable         # G2-item

# Read committed lets transactions see half of another's effects.
adya run sim -i read-committed -c snapshot-isolation       # G-single-item

# A buggy "snapshot" that writes back stale state.
adya run sim -i lost-update -c read-committed              # G1a, incompatible-order, ...

Checking an existing history

adya check -m list-append -c serializable history.jsonl
adya check -m rw-register -c snapshot-isolation history.edn
adya check --json history.jsonl     # machine-readable report

Exit status is 0 if the history satisfies every requested model, 1 if anomalies were found, 2 if the result is unknown (for example, no dependencies could be inferred, or cycle search timed out), and 3 on error.

A history is a sequence of operations, each a transaction invocation or completion on a process:

{"index":0,"type":"invoke","process":0,"value":[["append",1,1],["r",2,null]]}
{"index":1,"type":"ok","process":0,"value":[["append",1,1],["r",2,[3,7]]]}

• type is invoke, then ok (committed), fail (definitely aborted) or info (unknown).
• list-append micro-ops are ["append", key, value] and ["r", key, [elements...]]. Appended values must be unique per key. This is the workload to use if you can: every read reveals the order of all the appends before it, so adya can recover the full version order.
• rw-register micro-ops are ["w", key, value] and ["r", key, value]. Registers hide their history, so far less can be inferred. adya knows the initial nil precedes everything; you can let it assume more: --wfr-keys (a transaction's writes follow its reads), --sequential-keys (process order implies version order), --linearizable-keys (real-time order does), or hand it the database's own commit order with --transaction-order order.json.

Consistency models include strict-serializable (default), serializable, snapshot-isolation, repeatable-read, read-committed, read-uncommitted, their strong-session-* and strong-* variants, cursor-stability, consistent-view, update-serializable, and others; see adya check --help.

Testing a database

adya run sqlite   --url test.sqlite -i immediate
adya run postgres --url postgres://user:pass@localhost/db -i serializable
adya run mysql    --url mysql://user:pass@localhost/db    -i repeatable-read -c snapshot-isolation

Each run creates two tables, adya_lists (k, v) and adya_regs (k, v), and runs --txns random transactions (default 2000) from --processes concurrent clients (default 8) over a small, rotating pool of --keys hot keys. Appends are upserts that concatenate onto a text column. Errors before COMMIT are recorded as failures; losing the connection during COMMIT is recorded as indeterminate, and that client reconnects under a new process id, as in Jepsen. The history is written to history.jsonl (-o to change it) and checked against -c.

What it finds

CI runs scripts/databases.sh against Postgres 17 and MySQL 8.4 on every push: 4,000 transactions from 10 clients over 6 hot keys, per isolation level and workload, each history checked against a ladder of models. Cells list the anomaly types found, or "valid". From one run (list-append workload):

Postgres behaves as documented: its REPEATABLE READ is snapshot isolation, which permits write skew (G2-item), and its SERIALIZABLE came out strict serializable. MySQL's REPEATABLE READ is another story: it permits lost updates and read skew, so it is not snapshot isolation, nor even repeatable read in Adya's sense. Jepsen reported the same of MySQL 8.0.34 in 2023; adya reproduces it from a clean start in a few seconds.

Faults

Isolation bugs often hide in failure paths, so adya run can break things while it works. Give it a command that injects a fault and one that heals it; a nemesis thread runs them on a schedule and records each in the history, as Jepsen does:

adya run postgres --url "$PG" -i serializable -n 6000 -p 10 \
  --fault "docker restart -t 0 pg" --heal "true" --fault-every 3 --fault-for 1

Anything a shell can do works: docker pause/unpause, kill -STOP, pg_terminate_backend, iptables, tc netem, a toxiproxy toggle. Clients replace dead connections and retry connecting for up to 30 seconds, so a restarting database doesn't end the run. In CI, Postgres SERIALIZABLE restarted nine times during a 6,000-transaction run (2,957 committed, 3,043 failed or aborted) still checks as strict serializable.

Any other database: adya run exec

adya run exec --url "python my_client.py" -c serializable

adya starts the command once per client and writes one line per transaction to its stdin:

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

The client runs it as one transaction and answers with one line:

{"type":"ok","value":[["append",3,7],["r",4,[1,7]]]}
{"type":"fail","error":"serialization failure"}
{"type":"info","error":"connection reset during commit"}

Use fail only when the transaction certainly did not commit. For rw-register workloads (-m rw-register) reads return a number or null. examples/exec_sqlite.py is a complete client in about 60 lines of Python; CI runs it on every push.

Using the library

use adya::{check, History, Opts, Valid, Workload};

let history = History::parse(&std::fs::read_to_string("history.edn")?)?;
let report = check(&history, Workload::ListAppend, &Opts {
    models: vec!["serializable".into()],
    ..Opts::default()
});
if report.valid == Valid::False {
    for (kind, anomalies) in &report.anomalies {
        for a in anomalies {
            eprintln!("{kind}:\n{}", a.explanation);
        }
    }
}

adya::run and adya::db expose the workload runner and drivers; implement adya::run::Client (one method: run a transaction, report how it ended) to test a database from Rust.

How it works

1. Parse the history and pair each invocation with its completion.
2. Infer version orders. For list-append, each key's longest read is its version order; reads that aren't prefixes of each other are themselves an anomaly (incompatible-order). For rw-register, the order comes from the initial state and, optionally, writes-follow-reads.
3. Find direct anomalies that need no graph: aborted reads (G1a), intermediate reads (G1b), reads inconsistent with the transaction's own writes (internal), duplicated elements, dirty updates, lost updates.
4. Build Adya's dependency graph over committed (and possibly committed) transactions: ww (installed the next version), wr (read what the other wrote), rw (read a version the other overwrote). When the requested models need it, add process order or real-time order. Real-time order uses a transitive reduction (each transaction links only to the frontier of recent completions), so it stays linear in the history.
5. Bound what is possible. For each model, check whether the subgraph it forbids cycles in has a nontrivial strongly connected component at all. This is cheap, and it rules out whole families of anomalies before any search.
6. Search for the worst anomaly first. Inside each SCC, run a breadth-first search over (transaction, path-state) pairs, where the path state tracks how many rw edges the path has used, whether two were adjacent, and whether it has used a wr or a real-time edge. One search then finds, say, a shortest cycle with exactly one anti-dependency (G-single), with only nonadjacent ones (G-nonadjacent), or with an adjacent pair (G2-item). Anything implied by what was found is skipped.
7. Report each cycle with a proof that names the key and value behind every edge, plus the weakest models the anomalies rule out (not) and everything stronger (also not).

Is it right?

The checker is held to three independent standards in CI:

• Elle's expected results. elle-cli ships histories with the verdicts Elle produced for them. adya matches all 56 list-append and rw-register cases on verdict, anomaly types and the weakest models ruled out (scripts/compare_elle_results.py).
• Elle itself, live. On every push, CI generates random histories across isolation levels and workloads, and checks each one with both adya and the JVM Elle (scripts/differential.py). In the first full run, 40 histories of 300 transactions each: every one of the 34 that Elle finished got an identical answer from adya. Elle could not finish the other six: five hit the 5-minute limit and one exhausted a 6 GB heap, all from the read-uncommitted and broken-snapshot simulations, whose histories are dense with anomalies. adya checked all 40 in 0.2 seconds in total.
• Databases with known answers. The simulated database implements serializable, snapshot isolation, read committed (with write locks), read uncommitted, and a broken snapshot mode. Tests assert, over thousands of transactions per seed, that correct runs produce no anomalies at their level and that the expected anomalies do appear above it (tests/sim.rs).

Limitations

• Predicate workloads (and so the predicate variants G2/G-single proper, as opposed to the item variants) and Elle's other checkers (bank, set, long fork, counters) are out of scope for now.
• No graph rendering. Each anomaly comes with a textual proof and JSON detail instead of Graphviz plots.
• The SQL drivers connect without TLS.
• --sequential-keys / --linearizable-keys walk forward from every transaction for every key it touched; on very long histories where keys go cold this is quadratic.
• A clean result means no anomaly was observed in this history. It is not a proof that the database is correct. Run longer, with more contention (fewer --keys), and with faults.

Roadmap

• Built-in nemeses (client kills, a partitioning proxy) on top of the command-driven ones.
• Predicate reads (G2 and G-single proper).
• A linearizability checker for single-object histories.
• --directory output with per-anomaly files and DOT graphs, as in Elle.

Credits

The analysis follows Atul Adya's Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions (MIT, 1999) and Kingsbury & Alvaro's Elle: Inferring Isolation Anomalies from Experimental Observations (VLDB 2020). Anomaly and model names follow Elle's so reports from the two tools can be compared directly. adya is an independent implementation and is not affiliated with Jepsen.

License

MIT or Apache-2.0, at your option.