Expand description
adya: a black-box checker for transactional isolation.
Give it a history of transactions a database executed, and it infers the dependency graph between them (Adya’s write-write, write-read and read-write edges, plus process and real-time order), then hunts for the cycles that each isolation level forbids.
use adya::{check, History, Opts, Valid, Workload};
// Two transactions each read both keys as empty, then append to a
// different one: write skew, legal under snapshot isolation only.
let h = History::from_json(r#"
{"type":"invoke","process":0,"value":[["r","x",null],["r","y",null],["append","x",1]]}
{"type":"invoke","process":1,"value":[["r","x",null],["r","y",null],["append","y",1]]}
{"type":"ok","process":0,"value":[["r","x",[]],["r","y",[]],["append","x",1]]}
{"type":"ok","process":1,"value":[["r","x",[]],["r","y",[]],["append","y",1]]}
"#).unwrap();
let serializable = Opts { models: vec!["serializable".into()], ..Opts::default() };
let r = check(&h, Workload::ListAppend, &serializable);
assert_eq!(r.valid, Valid::False);
assert_eq!(r.anomaly_types, ["G2-item"]);
let si = Opts { models: vec!["snapshot-isolation".into()], ..Opts::default() };
assert_eq!(check(&h, Workload::ListAppend, &si).valid, Valid::True);Re-exports§
pub use check::check;pub use check::Anomaly;pub use check::Opts;pub use check::Report;pub use check::Valid;pub use check::Workload;pub use history::History;
Modules§
- check
- Turning a workload’s dependency graph into a verdict.
- db
- Database clients for the workload runner.
- gen
- Random transaction workloads in the style of Elle’s generators: a small pool of hot keys, short transactions mixing reads and writes, unique values per key, and keys retired after enough writes so reads stay short.
- graph
- Transaction dependency graphs and the cycle search over them.
- history
- Histories: what clients asked the database to do, and what came back.
- list_
append - The list-append workload: transactions append unique elements to lists and read whole lists back.
- model
- Consistency models, the anomalies they forbid, and how both relate.
- run
- Running a generated workload against a real database and recording the history.
- rw_
register - The rw-register workload: transactions read registers and blindly overwrite them with unique values.
- sim
- A deterministic in-memory database for exercising the checker.