{"_id":"@botiroff/adya","_rev":"2-40af55ff0246a247bc4f524309ca344c","name":"@botiroff/adya","dist-tags":{"latest":"0.2.0"},"versions":{"0.1.0":{"name":"@botiroff/adya","version":"0.1.0","keywords":["transactions","isolation-levels","serializability","mvcc","snapshot-isolation","ssi","write-skew","linearizability","elle","jepsen","database-internals"],"author":{"name":"BOTIROFF-D"},"license":"MIT","_id":"@botiroff/adya@0.1.0","maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"homepage":"https://github.com/BOTIROFF-D/adya#readme","bugs":{"url":"https://github.com/BOTIROFF-D/adya/issues"},"dist":{"shasum":"32d794650504e4ea1bbf601a3b9db8f2c08a35f4","tarball":"https://registry.npmjs.org/@botiroff/adya/-/adya-0.1.0.tgz","fileCount":7,"integrity":"sha512-CqoMkfrKE4dddCx6o1ctGxLK/Uf13572/ZjEGibwW4DUsmkq98BnF6v+HvoV0U7P3awRQ7k8aFv7wvQSLXz13w==","signatures":[{"sig":"MEUCIGQTky/RddN6UUc3ik45EFiIu8JBrCGjYQ8P3Cl5P7t/AiEAgoJgra3yfyiQ0+e53fGVYG0J2X4PAaIadIoerOphKB0=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":82374},"main":"./dist/index.cjs","type":"module","types":"./dist/index.d.ts","module":"./dist/index.js","engines":{"node":">=18"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js","require":"./dist/index.cjs"}},"gitHead":"d1f7a241ac5e4a1e3d6d340996317b3b4cad8dea","scripts":{"test":"vitest run","build":"tsup","museum":"vitest run museum","prepare":"npm run build","typecheck":"tsc --noEmit","test:watch":"vitest","prepublishOnly":"npm run typecheck && npm run test && npm run build"},"_npmUser":{"name":"botiroff","email":"thebotiroff@gmail.com"},"repository":{"url":"git+https://github.com/BOTIROFF-D/adya.git","type":"git"},"_npmVersion":"11.11.0","description":"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.","directories":{},"sideEffects":false,"_nodeVersion":"25.8.1","publishConfig":{"access":"public"},"_hasShrinkwrap":false,"devDependencies":{"tsup":"^8.3.5","vitest":"^2.1.8","unflake":"^0.3.0","typescript":"^5.7.2","@types/node":"^22.10.2"},"peerDependencies":{"unflake":"^0.3.0"},"_npmOperationalInternal":{"tmp":"tmp/adya_0.1.0_1786788664989_0.2125776631922518","host":"s3://npm-registry-packages-npm-production"}},"0.2.0":{"name":"@botiroff/adya","version":"0.2.0","description":"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.","keywords":["transactions","isolation-levels","serializability","mvcc","snapshot-isolation","ssi","write-skew","linearizability","elle","jepsen","database-internals"],"license":"MIT","author":{"name":"BOTIROFF-D"},"repository":{"type":"git","url":"git+https://github.com/BOTIROFF-D/adya.git"},"homepage":"https://github.com/BOTIROFF-D/adya#readme","bugs":{"url":"https://github.com/BOTIROFF-D/adya/issues"},"type":"module","sideEffects":false,"publishConfig":{"access":"public"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js","require":"./dist/index.cjs"}},"main":"./dist/index.cjs","module":"./dist/index.js","types":"./dist/index.d.ts","engines":{"node":">=18"},"scripts":{"build":"tsup","typecheck":"tsc --noEmit","test":"vitest run","test:watch":"vitest","museum":"vitest run museum","prepare":"npm run build","prepublishOnly":"npm run typecheck && npm run test && npm run build","test:postgres":"vitest run against-postgres"},"peerDependencies":{"unflake":"^0.3.0"},"devDependencies":{"@types/node":"^22.10.2","@types/pg":"^8.21.0","pg":"^8.23.0","tsup":"^8.3.5","typescript":"^5.7.2","unflake":"^0.3.0","vitest":"^2.1.8"},"gitHead":"00ff1d96a74da9500de238509dc4da9a58097d91","_id":"@botiroff/adya@0.2.0","_nodeVersion":"25.8.1","_npmVersion":"11.11.0","dist":{"integrity":"sha512-/+UZ1N6DINgvBZ58inefGEWLJwHv9sADtTRTB73s04cP4fqIHv6U3EGSUvKIIG6VNJ34UABdU93kOPMp89Ok/w==","shasum":"f2a46c14afb162293ebac01595afea879d0dc558","tarball":"https://registry.npmjs.org/@botiroff/adya/-/adya-0.2.0.tgz","fileCount":7,"unpackedSize":85398,"signatures":[{"keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U","sig":"MEQCIH/adTMBH0dt3WrbBvtHkR964APJ3JdwkqN0N4h5IynSAiBzAzekngGBRoe4ItRbUtlPiVgPL78lNo/Gtg/UMS7Iew=="}]},"_npmUser":{"name":"botiroff","email":"thebotiroff@gmail.com"},"directories":{},"maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"_npmOperationalInternal":{"host":"s3://npm-registry-packages-npm-production","tmp":"tmp/adya_0.2.0_1786941012031_0.5062379883151138"},"_hasShrinkwrap":false}},"time":{"created":"2026-08-15T10:11:04.842Z","modified":"2026-08-17T04:30:12.388Z","0.1.0":"2026-08-15T10:11:05.115Z","0.2.0":"2026-08-17T04:30:12.177Z"},"bugs":{"url":"https://github.com/BOTIROFF-D/adya/issues"},"author":{"name":"BOTIROFF-D"},"license":"MIT","homepage":"https://github.com/BOTIROFF-D/adya#readme","keywords":["transactions","isolation-levels","serializability","mvcc","snapshot-isolation","ssi","write-skew","linearizability","elle","jepsen","database-internals"],"repository":{"type":"git","url":"git+https://github.com/BOTIROFF-D/adya.git"},"description":"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.","maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"readme":"# adya\n\n**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.\n\n[![CI](https://github.com/BOTIROFF-D/adya/actions/workflows/ci.yml/badge.svg)](https://github.com/BOTIROFF-D/adya/actions/workflows/ci.yml)\n[![npm](https://img.shields.io/npm/v/%40botiroff%2Fadya)](https://www.npmjs.com/package/@botiroff/adya)\n![node](https://img.shields.io/badge/node-%E2%89%A518-blue)\n![license](https://img.shields.io/badge/license-MIT-blue)\n\nNamed for [Atul Adya](https://pmg.csail.mit.edu/papers/adya-phd.pdf), whose 1999 thesis replaced the ANSI standard's prose definitions of isolation levels with the phenomena this repository implements and detects.\n\n---\n\nEvery database advertises isolation levels. Almost nobody can show you what theirs actually admits.\n\nThe 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.\n\n## The ladder\n\n```\nread-uncommitted     sound over 150 schedules   admits G1b at seed 0\nread-committed       sound over 150 schedules   admits G-single at seed 1\nsnapshot-isolation   sound over 150 schedules   admits G2-item at seed 25\nserializable         sound over 150 schedules   admits nothing, commits 51%\n```\n\nEach rung is held to two things:\n\n**Sound** — over hundreds of seeded schedules, the engine at level L never produces an anomaly L is required to prevent.\n\n**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.\n\nThe 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.\n\n**Neither side is trusted alone. Each convicts the other.**\n\nThe 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.\n\n## Checked against a database somebody else wrote\n\nEverything 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.\n\nSo 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`](./src/store/mvcc.ts) implements.\n\n**The directed write-skew scenario.** Two transactions, each reading what the other is about to write:\n\n| PostgreSQL level | Outcome | Checker's verdict |\n| --- | --- | --- |\n| `READ COMMITTED` | both commit | **G2-item** `T2 —rw→ T1 —rw→ T2` |\n| `REPEATABLE READ` | both commit | **G2-item** — clean as snapshot isolation, violation as serializable |\n| `SERIALIZABLE` | one aborted | nothing |\n\n**A random sweep**, 25 rounds of three concurrent transactions each:\n\n| PostgreSQL level | Aborts | Anomalies found |\n| --- | --- | --- |\n| `READ COMMITTED` | 0 / 100 | **G-single × 24** |\n| `REPEATABLE READ` | 32 / 100 | none |\n| `SERIALIZABLE` | 32 / 100 | none |\n\nRead that table against [the ladder](#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.\n\nPostgreSQL 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/`](./against-postgres) and see the same thing.\n\n```bash\nnpm run test:postgres     # ADYA_PG=postgres://... to point elsewhere\n```\n\n## What the phenomena are\n\nFrom Adya §3, and used here by their own names so a reader can check this against the source rather than against my paraphrase.\n\n| | |\n| --- | --- |\n| **G0** | a cycle of write-dependencies alone |\n| **G1a** | a read of a value written by a transaction that then aborted |\n| **G1b** | a read of a value its writer replaced later in the same transaction |\n| **G1c** | a cycle of write- and read-dependencies |\n| **G-single** | a cycle containing exactly one anti-dependency — read skew |\n| **G2-item** | a cycle containing more than one — write skew |\n\nEach level forbids everything the level below it forbids, plus one more:\n\n| Level | Adds |\n| --- | --- |\n| read uncommitted | G0 |\n| read committed | G1a, G1b, G1c |\n| snapshot isolation | G-single |\n| serializable | G2-item |\n\nThe 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/`](./src/check).\n\n## How the checker can know\n\nTo 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.\n\nSo 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.\n\nThat idea is the core of [Elle](https://github.com/jepsen-io/elle) (Kingsbury & Alvaro, VLDB 2020) and this borrows it wholesale.\n\nWith 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.\n\nEach 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.\n\n## How the engine differs by level\n\nOne 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.\n\n```\nread-uncommitted     reads see other transactions' buffered writes\nread-committed       reads see the latest committed version, each time\nsnapshot-isolation   reads see the snapshot at start; first committer wins\nserializable         the above, plus Cahill's SSI\n```\n\nAppends 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.\n\n**SSI** follows [Cahill, Röhm and Fekete (SIGMOD 2008)](https://dl.acm.org/doi/10.1145/1376616.1376690), 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.\n\n## Usage\n\n```bash\nnpm install @botiroff/adya\n```\n\nOr to work on it:\n\n```bash\nnpm install\nnpm test        # engine and checker\nnpm run museum  # the ladder\n```\n\n```ts\nimport { Store, checkHistory } from \"@botiroff/adya\";\n\nconst store = new Store();\nstore.begin(\"t1\", \"serializable\");\nstore.read(\"t1\", \"x\");\nstore.append(\"t1\", \"y\");\nstore.commit(\"t1\");\n\nconst report = checkHistory(store.history, \"serializable\");\n// { ok: true, violations: [], observed: [], stats: { ... } }\n```\n\nThe 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.\n\n## Limits\n\n**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.\n\n**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.\n\n**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.\n\n**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.\n\nFor the smallest instance the theorem is available: [pnueli](https://github.com/BOTIROFF-D/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.\n\n**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.\n\n## Prior art\n\nThe phenomena and their numbering are [Adya's thesis](https://pmg.csail.mit.edu/papers/adya-phd.pdf) (MIT, 1999), which formalised what [Berenson et al.](https://arxiv.org/abs/cs/0701157) had shown was wrong with the ANSI SQL definitions in 1995. Serializable snapshot isolation is [Cahill, Röhm and Fekete](https://dl.acm.org/doi/10.1145/1376616.1376690) (SIGMOD 2008). The list-append trick that makes version order recoverable is [Elle](https://github.com/jepsen-io/elle) (Kingsbury & Alvaro, VLDB 2020), the checker [Jepsen](https://jepsen.io/) uses to find these anomalies in real databases.\n\nSchedules are made reproducible by [unflake](https://github.com/BOTIROFF-D/unflake).\n\n## Who wrote this\n\n[Doniyor Botirov](https://dbit.one/en/founder), founder of [dbit.one](https://dbit.one/en). 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](https://dbit.one/en/blog/transaction-isolation-levels-anomalies).\n\n## License\n\nMIT\n","readmeFilename":"README.md"}