Metadata-Version: 2.4
Name: isolab
Version: 0.1.0
Summary: Deterministic PostgreSQL transaction-isolation anomaly lab (inspired by Designing Data-Intensive Applications, ch. 7)
Author: Daniel Kuboi
License-Expression: MIT
Project-URL: Homepage, https://github.com/Dan9el8/isolab
Project-URL: Repository, https://github.com/Dan9el8/isolab
Project-URL: Issues, https://github.com/Dan9el8/isolab/issues
Project-URL: Changelog, https://github.com/Dan9el8/isolab/releases
Keywords: postgresql,transactions,isolation-levels,concurrency,write-skew,serializable,testing,ddia
Classifier: Development Status :: 3 - Alpha
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Database
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: psycopg[binary]>=3.1
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == "dev"
Dynamic: license-file

# 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](#1-why-this-exists)
2. [Results](#2-results-postgresql-16)
3. [Quick start](#3-quick-start)
4. [CLI reference](#4-cli-reference)
5. [How it works](#5-how-it-works)
6. [Scenario catalogue](#6-scenario-catalogue)
7. [Writing your own scenario](#7-writing-your-own-scenario)
8. [Testing and CI](#8-testing-and-ci)
9. [Limitations (read this)](#9-limitations-read-this)
10. [Roadmap](#10-roadmap)
11. [Project layout](#11-project-layout)
12. [References](#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](#6-scenario-catalogue)).
- 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`](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](#63-phantom-double-booked-room)).
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]`.

```bash
# 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:

```bash
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

```text
$ 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.

```text
 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`:

```text
 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. |

```bash
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](#63-phantom-double-booked-room).

---

## 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](#56-a-subtlety-that-affects-results-when-the-snapshot-is-taken) 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`):

```python
# 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`:

```python
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

```bash
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.
