isolab — a deterministic PostgreSQL isolation-anomaly lab

Most engineers can recite "ACID". Far fewer can say which concurrency bugs their database still allows at their isolation level. isolab answers that with evidence: it forces the exact unlucky interleaving against a real PostgreSQL server, checks a business invariant afterwards, and prints a matrix of scenario × fix × isolation level.

Inspired by Chapter 7 (Transactions) of Martin Kleppmann's Designing Data-Intensive Applications, which argues that "ACID" is vague in practice and that weak isolation causes silent data corruption. This repo turns that argument into something you can run, diff across Postgres versions, and extend with bugs from your own systems.

                                        READ COMMITTED   REPEATABLE READ  SERIALIZABLE

Write skew (on-call doctors)  [DDIA ch. 7, 'Write Skew and Phantoms']
  bug: naive                            ✘ ANOMALY        ✘ ANOMALY        ⛔ aborted
  fix: for_update                       ✔ safe           ⛔ aborted        ⛔ aborted

(Real output, PostgreSQL 16.15. Full matrix below.)

---

Contents

1. Why this exists
2. Results
3. Quick start
4. CLI reference
5. How it works
6. Scenario catalogue
7. Writing your own scenario
8. Testing and CI
9. Limitations (read this)
10. Roadmap
11. Project layout
12. References

---

1. Why this exists

Concurrency bugs caused by weak isolation are silent. Nothing crashes. Two requests succeed, each doing something reasonable on its own, and the combination breaks a rule nobody wrote a test for:

• two doctors both go off call, leaving none on duty;
• two payouts both pass a balance check and the wallet goes negative;
• the same payment callback is delivered twice and credits a wallet twice;
• a meeting room is booked by two people for overlapping hours.

They rarely show up in development because a single developer never produces the overlap. They show up in production under load, intermittently, which makes them very expensive to diagnose.

The usual testing approach, "spawn N threads and hope", passes by luck. This tool takes the opposite approach: control the interleaving exactly, so a bug is either provably reachable at a given isolation level or provably not.

What you get:

• A reproducible answer to "does my fix actually work at the isolation level I run in production?" (spoiler: several well-known fixes only work at some levels, see §6).
• A regression test for database upgrades or config changes (isolab verify exits non-zero if any behaviour differs from the documented expectation).
• A teaching tool: --trace prints the exact SQL timeline of any cell.

---

2. Results (PostgreSQL 16)

Generated by isolab run --no-retry against PostgreSQL 16.15. Every cell was also run repeatedly (isolab verify --repeat 10) with identical results each time; the interleavings are deterministic. The full report with observed violation messages is in docs/RESULTS.md.

Scenario	Variant	READ COMMITTED	REPEATABLE READ	SERIALIZABLE
Lost update	naive (bug)	❌ ANOMALY	⛔ aborted	⛔ aborted
	atomic_update	✅ safe	⛔ aborted	⛔ aborted
	for_update	✅ safe	⛔ aborted	⛔ aborted
	optimistic_version	⛔ aborted	⛔ aborted	⛔ aborted
Write skew	naive (bug)	❌ ANOMALY	❌ ANOMALY	⛔ aborted
	for_update	✅ safe	⛔ aborted	⛔ aborted
Phantom (double booking)	naive (bug)	❌ ANOMALY	❌ ANOMALY	⛔ aborted
	exclusion_constraint	⛔ aborted	⛔ aborted	⛔ aborted
	lock_room	✅ safe	❌ ANOMALY	⛔ aborted
Read skew	naive (bug)	❌ ANOMALY	✅ safe	✅ safe
Wallet overdraft	naive (bug)	❌ ANOMALY	⛔ aborted	⛔ aborted
	guarded_update	✅ safe	⛔ aborted	⛔ aborted
	check_constraint	⛔ aborted	⛔ aborted	⛔ aborted
Duplicate M-Pesa callback	naive (bug)	❌ ANOMALY	❌ ANOMALY	⛔ aborted
	unique_constraint	⛔ aborted	⛔ aborted	⛔ aborted
	idempotent_insert	✅ safe	⛔ aborted	⛔ aborted

How to read a cell

Symbol	Meaning
✅ safe	No transaction was rejected and the invariant holds.
⛔ aborted	The database (or an app-level check) rejected a transaction. The invariant holds, but your application received an error and must retry.
🔁 retried	Default mode: the aborted transaction was re-run from scratch, the way a well-behaved app would, and succeeded. Same as ⛔ plus proof that retrying works.
❌ ANOMALY	The invariant was violated. Real data corruption.

What the matrix teaches

1. PostgreSQL's REPEATABLE READ is snapshot isolation. It stops read skew and lost updates (by aborting the loser), but write skew and phantoms sail straight through. This is the single most common surprise.
2. Only SERIALIZABLE protects the naive code, and it does so by aborting. Using it means writing retry logic. A ⛔ is not "free": it is an error path you must handle.
3. A fix is a (technique × isolation level) pair, not a technique. FOR UPDATE is safe at READ COMMITTED but turns into aborts at higher levels. lock_room is safe at READ COMMITTED yet fails at REPEATABLE READ (see §6.3).
4. Constraints beat clever application logic. EXCLUDE, UNIQUE and CHECK give the same ⛔ result at all three levels, because they are enforced at write time regardless of what your snapshot saw.
5. Pushing the logic into one statement (SET value = value + 1, UPDATE … WHERE balance >= 80, INSERT … ON CONFLICT DO NOTHING) is the cheapest correct fix at READ COMMITTED, the default level.

---

3. Quick start

Requirements: Python 3.10+, and a PostgreSQL 14+ server you can freely use (see the warning below). The only Python dependency is psycopg[binary].

# 1. a throwaway Postgres on localhost:5433 (needs Docker)
make up

# 2. install
python -m venv .venv && source .venv/bin/activate
make install            # pip install -e ".[dev]"

# 3. run everything
isolab run

# 4. see exactly what happened in one cell
isolab run write_skew --variant naive --level rr --trace

No Docker? Point at any Postgres:

export ISOLAB_DSN="postgresql://user:pass@localhost:5432/scratch_db"
isolab run

⚠️ Use a scratch database. For every cell isolab runs DROP SCHEMA IF EXISTS isolab CASCADE and recreates it. It never touches other schemas, but don't point it at a database where a schema named isolab matters. It also runs CREATE EXTENSION IF NOT EXISTS btree_gist (a trusted extension on PostgreSQL 13+; if it can't be created, the one variant that needs it is skipped and reported as such). Do not run two isolab processes against the same database at once.

Example: tracing a bug

$ isolab run write_skew --variant naive --level rr --trace

--- write_skew / naive @ REPEATABLE READ ---
 1  A        read       BEGIN ISOLATION LEVEL REPEATABLE READ
                       SELECT count(*) FROM doctors WHERE on_call  ->  [(2,)]
 2  B        read       BEGIN ISOLATION LEVEL REPEATABLE READ
                       SELECT count(*) FROM doctors WHERE on_call  ->  [(2,)]
 3  A        write      UPDATE doctors SET on_call = false WHERE name = 'alice'  ->  1 row(s)
 4  B        write      UPDATE doctors SET on_call = false WHERE name = 'bob'  ->  1 row(s)
 5  A        commit     COMMIT
 6  B        commit     COMMIT
   result: ANOMALY - nobody is on call (write skew)

Same schedule at SERIALIZABLE: both writes succeed, then the second COMMIT fails.

 5  A        commit     COMMIT
 6  B        commit     COMMIT
                       ✘ serialization_failure: could not serialize access due to read/write dependencies among transactions
   result: ABORTED

And a fix that blocks, from lost_update / for_update @ READ COMMITTED:

 1  A        read       BEGIN ISOLATION LEVEL READ COMMITTED
                       SELECT value FROM counters WHERE id = 1 FOR UPDATE  ->  [(0,)]
 2  B        read       ⏸ txn B is waiting on a lock; schedule continues
 3  A        write      UPDATE counters SET value = 1 WHERE id = 1  ->  1 row(s)
 4  A        commit     COMMIT
 5  B        read       BEGIN ISOLATION LEVEL READ COMMITTED
                       SELECT value FROM counters WHERE id = 1 FOR UPDATE  ->  [(1,)]
 6  B        write      UPDATE counters SET value = 2 WHERE id = 1  ->  1 row(s)
 7  B        commit     COMMIT
   result: SAFE

Notice B's SELECT returns 1, not 0. Under READ COMMITTED a blocked FOR UPDATE re-reads the row after the lock is released, which is exactly why this fix works at that level.

---

4. CLI reference

isolab [--dsn DSN] <command> [options]

--dsn defaults to $ISOLAB_DSN, then postgresql://postgres:postgres@localhost:5433/isolab (the docker-compose.yml database).

Command	What it does
isolab list	List every scenario and its variants (bug vs fix).
isolab explain <scenario>	Print the story, each variant's exact schedule, and the documented result per level. No database needed.
isolab run [scenario ...]	Run cells and print the matrix.
isolab verify [scenario ...]	Run cells and exit 1 if any outcome differs from the documented expectation, or is non-deterministic.

Options for run and verify:

Option	Meaning
--variant KEY	Only this variant (naive, for_update, …).
--level L	Only one isolation level: rc, rr, ser (or "read committed", etc.).
--repeat N	Run every cell N times. Output shows ×N/N and flags any non-determinism.
--no-retry	Don't retry aborted transactions; report them as ⛔ aborted instead of 🔁 retried.

Options for run only:

Option	Meaning
--format table|markdown|json	Output format (default table).
-o, --output FILE	Write the report to a file.
--trace	Print the step-by-step SQL timeline of every selected cell.

isolab run                                       # everything, with retries
isolab run --no-retry                            # show raw aborts
isolab run lost_update mpesa_callback            # two scenarios
isolab run phantom_booking --variant lock_room --level rr --trace
isolab run --format json -o results.json         # for dashboards / diffing
isolab verify --repeat 20                        # CI gate

---

5. How it works

5.1 The problem with "spawn threads and hope"

A concurrency bug needs a specific interleaving, for instance A reads, B reads, A writes, B writes. Real threads hit it only occasionally, so a passing test proves nothing. isolab doesn't generate interleavings, it dictates them.

5.2 Architecture

                    ┌─────────────────────────────────────────────┐
  Variant           │  schedule: A.read  B.read  A.write  B.write │
  (scenario file)   │            A.commit  B.commit               │
                    └──────────────────────┬──────────────────────┘
                                           │ one step at a time
                                  ┌────────▼────────┐        ┌──────────────────┐
                                  │    Scheduler    │◄───────│ observer conn    │
                                  │ (main thread)   │ polls  │ pg_stat_activity │
                                  └───┬─────────┬───┘        └──────────────────┘
                          submit step │         │ submit step
                              ┌───────▼──┐   ┌──▼───────┐
                              │ Worker A │   │ Worker B │   one thread + one
                              │ conn #1  │   │ conn #2  │   PostgreSQL connection
                              └───────┬──┘   └──┬───────┘   per transaction
                                      └────┬────┘
                                      ┌────▼─────┐
                                      │PostgreSQL│
                                      └────┬─────┘
                       after all steps: ┌──▼───────────────────────┐
                                        │ retry aborted txns       │
                                        │ check invariant → outcome│
                                        └──────────────────────────┘

Each cell (scenario × variant × isolation level) runs in a freshly recreated schema:

1. Setup: create tables and seed rows.
2. Start workers: one thread and one real connection per transaction.
3. Run the schedule one step at a time (see 5.3).
4. Drain: wait for all workers to finish.
5. Retry any transaction that was aborted by a retryable error (see 5.5).
6. Check the invariant on a separate connection and classify the outcome.

5.3 Deterministic scheduling with lock detection

Releasing steps strictly in order has one catch: some steps block. In the "locking" fixes, B's SELECT … FOR UPDATE must wait for A. A naive scheduler would wait forever.

The scheduler therefore asks PostgreSQL itself. While waiting for a step to finish it polls pg_stat_activity.wait_event_type for that backend. If the backend is waiting on a Lock, the step is recorded as ⏸ blocked and the schedule moves on. The blocked step completes later, when the lock holder commits or rolls back.

There are no sleeps or timing guesses. After every step the scheduler also settles: it waits until every worker is either idle or lock-blocked. This guarantees that anything a commit unblocked has fully run before the next scheduled step starts. That is what makes 10 repeats give 10 identical results.

5.4 Outcomes

After the schedule finishes, the scenario's invariant function inspects the database (and the values each transaction observed) and returns a list of violations.

Condition	Outcome
any violation	ANOMALY
a transaction was rejected, none retried or retry failed	ABORTED
a transaction was rejected, retry succeeded, invariant holds	RETRIED
nothing rejected, invariant holds	SAFE
a transaction died with an unexpected error	ERROR (harness bug or unsupported situation)

Invariants are written against what actually committed. For example, the lost-update invariant is "counter equals the number of transactions that committed an increment", not "counter equals 2". Otherwise a correctly aborted transaction would be misreported as an anomaly.

5.5 Retry model

A rejected transaction counts as prevented, but a real application must then re-run it. To prove that the fix is complete, isolab retries rejected transactions after the schedule has finished (up to 3 attempts, one after another, each in a fresh transaction at the same isolation level) and re-evaluates the invariant.

Retryable errors: 40001 serialization_failure, 40P01 deadlock_detected, 23505 unique_violation, 23P01 exclusion_violation, 23514 check_violation, and the library's own AppConflict (used for optimistic-lock version mismatches).

Because each step re-reads state, the retried transaction takes the correct branch. For example, the second doctor now sees only one doctor on call and declines to go off call. Pass --no-retry to skip this and see the raw ⛔.

5.6 A subtlety that affects results: when the snapshot is taken

In REPEATABLE READ and SERIALIZABLE, PostgreSQL takes the transaction's snapshot at the first statement, not at BEGIN. isolab issues BEGIN ISOLATION LEVEL … lazily as part of each transaction's first step, so the first step of the schedule is where the snapshot is fixed. This matters for the lock_room result in §6.3.

---

6. Scenario catalogue

Every scenario defines: the story, the invariant it protects, the interleaving that breaks it, and a set of variants (naive code plus candidate fixes). Run isolab explain <scenario> for the exact schedules.

6.1 Lost update

Two transactions read a counter, add one in application code, write it back. Invariant: counter equals the number of committed increments.

Schedule: A.read B.read A.write A.commit B.write B.commit

Variant	RC	RR	SER	Why
naive	❌	⛔	⛔	At READ COMMITTED B overwrites A's value with a stale 0 + 1. At RR/SER, PostgreSQL detects that B's snapshot is stale and aborts it ("could not serialize access due to concurrent update").
atomic_update	✅	⛔	⛔	SET value = value + 1 makes the read-modify-write a single statement. At RC, B waits for A's row lock, then re-evaluates against the new value.
for_update	✅	⛔	⛔	B's locking SELECT waits, then (at RC) re-reads the committed value. At RR/SER it can't proceed on a row changed since its snapshot, so it aborts.
optimistic_version	⛔	⛔	⛔	WHERE version = <read> matches zero rows, the app raises AppConflict. At RR/SER the database aborts first. Always correct, always needs a retry loop.

6.2 Write skew (on-call doctors)

The book's canonical example. Alice and Bob are on call; each may go off call if at least two doctors are on call. Invariant: at least one doctor stays on call.

Schedule: A.read B.read A.write B.write A.commit B.commit

Variant	RC	RR	SER	Why
naive	❌	❌	⛔	Each transaction updates a different row, so there is no write-write conflict for snapshot isolation to detect. Only SERIALIZABLE's read/write dependency tracking catches it.
for_update	✅	⛔	⛔	Locking every on-call row while counting forces B to wait. At RC, B then re-evaluates and sees one doctor, so it declines. At RR it aborts.

6.3 Phantom (double-booked room)

Alice books room 1 for 09–11, Bob for 10–12. Each first checks that no overlapping booking exists. Invariant: bookings of the same room never overlap.

Schedule: A.check B.check A.book B.book A.commit B.commit (lock_room adds a leading lock step per transaction.)

Variant	RC	RR	SER	Why
naive	❌	❌	⛔	The conflicting row doesn't exist yet when either transaction checks, so there is nothing to lock or conflict with. This is a phantom.
exclusion_constraint	⛔	⛔	⛔	EXCLUDE USING gist (room_id WITH =, int4range(start_hour, end_hour) WITH &&) makes the database enforce non-overlap. B's insert blocks on A's uncommitted row, then fails with exclusion_violation. Works at every level.
lock_room	✅	❌	⛔	The interesting one. Materializing the conflict by locking the parent rooms row works at READ COMMITTED. At REPEATABLE READ it fails: B's snapshot was fixed at its first statement (the blocked lock request), before A committed, so after B finally gets the lock its overlap check still can't see A's booking.

The lock_room row is why §5.6 exists: "take a lock before reading" is only a fix if the snapshot is taken after the lock is acquired.

6.4 Read skew (non-repeatable read)

An auditor reads two accounts one after the other while a transfer moves 100 between them. Invariant: what the auditor sees must add up to 1000.

Schedule: R.read_checking T.transfer T.commit R.read_savings R.commit

Variant	RC	RR	SER	Why
naive	❌	✅	✅	At READ COMMITTED each statement gets a fresh snapshot, so the auditor sees 500 + 600 = 1100. REPEATABLE READ gives the whole transaction one snapshot, so the totals are consistent without any abort.

This is the one scenario where the fix is the isolation level. The only other fix is reading both balances in a single statement.

6.5 Wallet overdraft (double spend)

A wallet holds 100. Two payouts of 80 arrive together; each checks the balance first. Invariant: balance never negative, and equals opening balance + ledger.

Schedule: A.check B.check A.debit B.debit A.commit B.commit

Variant	RC	RR	SER	Why
naive	❌	⛔	⛔	Check and debit are separate statements. At RC both pass the check and the balance ends at −60.
guarded_update	✅	⛔	⛔	UPDATE … WHERE balance >= 80 plus a row-count check. The second payout is cleanly declined, with no error.
check_constraint	⛔	⛔	⛔	Naive code plus CHECK (balance >= 0). The database refuses the second debit; a retry then sees 20 and declines.

6.6 Duplicate payment callback (M-Pesa style)

Payment providers retry callbacks that aren't acknowledged quickly, so the same receipt can arrive at two workers concurrently. Each checks "have I seen this receipt?" before crediting. Invariant: a receipt credits the wallet at most once.

The wallet is modelled as an append-only ledger (balance = sum of rows), the event-sourced shape discussed in the book, which makes the race purely a check-then-insert problem.

Schedule: A.check B.check A.credit B.credit A.commit B.commit

Variant	RC	RR	SER	Why
naive	❌	❌	⛔	Both see "not seen yet" and both insert: receipt QGH7XYZ123 credited 2 times = 2000 for a single payment of 1000.
unique_constraint	⛔	⛔	⛔	A unique index on the receipt turns the duplicate into a unique_violation. Cheap and robust.
idempotent_insert	✅	⛔	⛔	INSERT … ON CONFLICT (mpesa_receipt) DO NOTHING with the receipt as an idempotency key. At RC the loser silently becomes a no-op.

---

7. Writing your own scenario

The most valuable use of this tool is encoding a bug from your own system. A scenario is a plain Python module. Here is the shape (condensed from isolab/scenarios/lost_update.py):

# isolab/scenarios/my_bug.py
from ..model import ABORTED, ANOMALY, SAFE, Scenario, Step, Variant

SETUP = [
    "CREATE TABLE counters (id int PRIMARY KEY, value int NOT NULL)",
    "INSERT INTO counters VALUES (1, 0)",
]

# A step is a function that receives a session `tx`.
#   tx.scalar(sql, *params) -> first column of first row
#   tx.rows(sql, *params)   -> list of tuples
#   tx.run(sql, *params)    -> affected row count (DML)
#   tx.ctx                  -> dict private to this transaction (carry values between steps)
def read(tx):
    tx.ctx["v"] = tx.scalar("SELECT value FROM counters WHERE id = 1")

def write(tx):
    tx.run("UPDATE counters SET value = %s WHERE id = 1", tx.ctx["v"] + 1)

# The invariant is called after the schedule with a session on the final state
# and a dict {txn_label: TxnResult(committed, ctx, ...)}. Return a list of violations.
def invariant(db, txns):
    committed = sum(t.committed for t in txns.values())
    value = db.scalar("SELECT value FROM counters WHERE id = 1")
    return [] if value == committed else [f"counter is {value}, {committed} committed"]

SCENARIO = Scenario(
    key="my_bug", title="My bug", summary="...", book_ref="...",
    setup=SETUP, invariant=invariant,
    variants=[
        Variant(
            key="naive", title="Read, add, write", description="...",
            txns={"A": [Step("read", read), Step("write", write)],
                  "B": [Step("read", read), Step("write", write)]},
            # The interleaving that breaks it. Each txn's steps appear once, in order,
            # followed by "commit".
            schedule=[("A", "read"), ("B", "read"), ("A", "write"), ("A", "commit"),
                      ("B", "write"), ("B", "commit")],
            # What you expect at each level. Run once, then record what you *understand*.
            expected={"READ COMMITTED": ANOMALY, "REPEATABLE READ": ABORTED,
                      "SERIALIZABLE": ABORTED},
            is_fix=False,
        ),
    ],
)

Then register it in isolab/scenarios/__init__.py:

from . import my_bug
ALL.append(my_bug.SCENARIO)   # or add it to the list literal

Rules, enforced when the module is imported:

• the schedule must mention every step of every transaction exactly once, in order, followed by commit, so a retry can replay a transaction from the top;
• expected must cover all three isolation levels with ANOMALY, ABORTED or SAFE;
• use %s for parameters;
• extra DDL for one variant (a constraint, an index) goes in Variant(setup=[...]);
• raise AppConflict from a step to model an application-level optimistic-lock failure;
• a variant that needs a contrib extension declares requires=("btree_gist",).

Good scenarios to add from real systems: an inventory oversell (stock >= 0), a "claim this job" queue (two workers dequeuing the same row; try FOR UPDATE SKIP LOCKED as the fix), a two-step-transfer deadlock, a username-uniqueness check-then-insert, or a double-spend on your wallet service.

---

8. Testing and CI

make test        # pytest: 59 tests (static validation + every cell of the matrix)
make verify      # isolab verify, exit code 1 on any mismatch

• tests/test_model.py checks that scenarios and schedules are well formed. No database needed.
• tests/test_matrix.py runs every (scenario, variant, level) cell and asserts it matches the documented expectation, and also asserts determinism (15 repeats of one cell) and the retry accounting. It skips itself if no server is reachable.
• .github/workflows/ci.yml runs the suite and isolab verify --repeat 3 against PostgreSQL 14, 15, 16 and 17. Because expectations are documented per cell, a behavioural change in a new Postgres release shows up as a failing test.

Status of verification: the full suite (59 tests) passes against PostgreSQL 16.15, and the 48-cell matrix verified identical across 10 consecutive repeats. The 14/15/17 CI matrix and docker-compose.yml are provided but have not been executed by the author yet. If a cell differs on your version, that is a finding worth a close look rather than something to paper over.

---

9. Limitations (read this)

Being clear about what this tool is not keeps its results trustworthy:

• It proves reachability, not probability. A forced interleaving shows that an anomaly can happen at a level. It says nothing about how often it happens under your real traffic.
• PostgreSQL only. Other engines implement the same level names very differently (for example, MySQL/InnoDB's REPEATABLE READ is not PostgreSQL's), so these results do not transfer.
• Two transactions per scenario. Real anomalies sometimes need three or more participants.
• It is not Jepsen. There is no fault injection, no network partitions, no multi-node cluster, and no history checker (Elle-style). It examines single-node transaction semantics only.
• The schedules are hand-written. The tool checks the interleavings you encode, not the interleavings that exist. A "safe" cell means this schedule was safe.
• SERIALIZABLE aborts can be false positives. PostgreSQL's SSI is conservative and may abort a transaction that would have been fine. Treat ⛔ at SERIALIZABLE as "must retry", never as proof the transactions truly conflicted.
• Invariants are yours. If an invariant is wrong or incomplete, a "safe" result is meaningless. Reviewing the invariant() function is part of reviewing a scenario.
• Retry is simplified. Retries run sequentially after the schedule, with up to three attempts, not under contention. It demonstrates that a retry converges to a correct state, not that your retry loop handles backoff or load.

---

10. Roadmap

• Stress mode: N workers with randomized interleavings, to measure how often an anomaly appears under load (complements the deterministic mode).
• More engines: MySQL/InnoDB and MongoDB transactions, to show the same anomaly behaving differently per engine.
• History checking: record transaction histories and check them with an Elle-style analysis instead of hand-written invariants.
• Three-transaction schedules and deadlock scenarios.
• Scenario DSL (YAML) for non-Python users.

---

11. Project layout

.
├── README.md
├── pyproject.toml            # installs the `isolab` command
├── docker-compose.yml        # throwaway Postgres 16 on :5433
├── Makefile                  # up / install / run / verify / test / report
├── docs/RESULTS.md           # generated report (make report)
├── .github/workflows/ci.yml  # verify against Postgres 14-17
├── isolab/
│   ├── model.py              # Scenario / Variant / Step + schedule validation
│   ├── engine.py             # sessions, workers, deterministic scheduler, retry, outcomes
│   ├── report.py             # table / markdown / json / trace renderers
│   ├── cli.py                # list | explain | run | verify
│   └── scenarios/
│       ├── lost_update.py
│       ├── write_skew.py
│       ├── phantom_booking.py
│       ├── read_skew.py
│       ├── wallet_overdraft.py
│       └── mpesa_callback.py
└── tests/
    ├── conftest.py           # skips integration tests if no database
    ├── test_model.py
    └── test_matrix.py

---

12. References

• Martin Kleppmann, Designing Data-Intensive Applications (O'Reilly, 2017), ch. 7 Transactions, and ch. 11 on idempotence.
• PostgreSQL documentation, Concurrency Control → Transaction Isolation and Explicit Locking.
• Hal Berenson et al., A Critique of ANSI SQL Isolation Levels (SIGMOD 1995): the paper that defined snapshot isolation and write skew.
• Dan R. K. Ports and Kevin Grittner, Serializable Snapshot Isolation in PostgreSQL (VLDB 2012): how PostgreSQL's SERIALIZABLE works.
• Kyle Kingsbury, Jepsen (jepsen.io): the inspiration for treating isolation claims as testable.