movie-ticket · PostgreSQL 18 · READ COMMITTED · jshell

Adya's isolation anomalies, tried against a live cinema booking app

A jshell script that tries to provoke every anomaly in Atul Adya's taxonomy through the public booking API of your own deployment of movie-ticket, and reports that none of them happens. This page is the manual: what each anomaly is, what it would look like at a cinema, why this app cannot produce it, and how to run the script yourself.

The script: adya-anomaly-probe.jsh (plain Java run by jshell, JDK 17 or newer). The fast path, once you have an empty showing and a signed-in cookie (steps below):

curl -fO https://dawud-tan.github.io/adya-anomaly-probe.jsh && chmod +x adya-anomaly-probe.jsh
export ADYA_SHOWING='https://<your-host>/halls/<hall-id>/showings/<showing-id>'
read -rs ADYA_COOKIE && export ADYA_COOKIE        # paste the Cookie header, press Enter
./adya-anomaly-probe.jsh

The short answer

The booking application never sets an isolation level, so every transaction runs at PostgreSQL's default, READ COMMITTED. That level alone rules out the first half of Adya's list: dirty writes (G0) and the three kinds of dirty read (G1a, G1b, G1c). It does not rule out the second half: lost updates (G-cursor), read skew (G-single), write skew (G2-item) and phantoms (G2). Those four are closed by the design, at each place where a booking depends on them:

an EXCLUDE constraint that makes a second live claim on a seat impossible to write;
three row locks: FOR UPDATE on the showing, FOR SHARE on the seats being booked, and FOR UPDATE on the customer before counting their seats;
state changes written as a single conditional UPDATE … WHERE status = …, never as a read followed by a write;
the seat map read in one SQL statement.

Why "loosening the isolation level" cannot make them appear here. The app already runs at the loosest level PostgreSQL has: READ UNCOMMITTED is accepted but behaves as READ COMMITTED. So the tests in the repository make an anomaly happen by removing the design protection instead, such as the constraint or the lock. For G0 and the G1 family nothing can make them happen, because PostgreSQL has no setting that permits them.

All the anomalies in one table

"Made to happen in" names the place where the anomaly actually occurs once its protection is removed. Test classes are in src/test/java/com/protek/booking/concurrency/ of the booking platform's repository.

Anomaly	At the cinema	What the script does	What stops it	Made to happen in
G0 write cycle	Two couples book the same pair; each goes home with one seat of it	`A3+A4` and `A4+A3`, twice each, released at the same instant	Row write locks (every PostgreSQL level); all-or-nothing holds	Nowhere: no PostgreSQL setting allows it
G1a aborted read	The seat map shows a claim from a booking that never went through	24 holds on a seat that is already held, each one's claim rolled back, while 3 viewers poll	MVCC: a rolled-back version is invisible	Nowhere
G1b intermediate read	Seats flicker to "held" during someone's failed block booking	24 five-seat holds whose last seat is taken, so four seats are written and withdrawn	MVCC: only the final committed version is visible	Nowhere
G1c circular information flow	Two couples see each other's half-made booking, both give up, the pair goes unsold	`A5+A6` and `A6+A5` at the same instant	The constraint check waits for an in-flight claim instead of reading it	Nowhere
G-cursor lost update (P4)	A customer cancels a seat and it stays sold; one barcode admits two people	Confirm an order and cancel one of its seats within a few ms, six rounds sweeping the offset	Conditional `UPDATE … WHERE status = …`, re-checked after the lock wait	A read-then-write in two statements; `AdmissionRescanConcurrencyTest` guards the scanner. No weakened twin in the tree
G-single read skew	The seat map shows half of someone's two-seat order	Hold a pair, then confirm it, while 3 viewers poll	The seat map is one SQL statement: one snapshot	Reading the pair with two statements at READ COMMITTED. No test in the tree
G2-item write skew	Two customers turn up with tickets for the same seat	8 holds on one seat at the same instant, three rounds	`EXCLUDE` constraint `reservation_no_overlap` (SQLSTATE `23P01`)	`SeatBookingConcurrencyDifferentialTest`: constraint dropped, all 8 succeed
G2 phantom / predicate	One scalper with two tabs gets past the 10-seats-a-day cap	One customer, two 5-seat holds on two showings of one day, at the same instant	The customer's row locked `FOR UPDATE` before counting	`DailyPurchaseCapConcurrencyDifferentialTest`: customer lock removed, all four holds land, 12 seats against a cap of 10
not Adya no cycle	A ticket sold for a showing that had already been cancelled	Not probed (needs a staff account)	`FOR UPDATE` on the showing row	`SessionCancellationRaceDifferentialTest`: plain `SELECT`, orphaned hold

Adya in five minutes

The ANSI SQL isolation levels are defined by three "phenomena": dirty read, non-repeatable read and phantom. These are worded in terms of locks, and they do not fit multiversion databases such as PostgreSQL. Atul Adya's 1999 MIT thesis, and the ICDE 2000 paper Generalized Isolation Level Definitions he wrote with Barbara Liskov and Patrick O'Neil, replaced them with conditions on the history of committed transactions. Any implementation can be checked against those conditions, whether it uses locking, MVCC or optimistic concurrency.

The history is drawn as a graph, the direct serialization graph. There is one node per committed transaction, and an edge from T1 to T2 whenever T2 depends on T1 in one of three ways:

ww write-dependency. T2 overwrote a version that T1 wrote.
wr read-dependency. T2 read a version that T1 wrote, or T1's write changed which rows T2's WHERE clause matched.
rw anti-dependency. T1 read a version and T2 then wrote the next one, or T2's write would have changed what T1's WHERE clause matched. T1 did not see T2, so T1 must come first.

A history is serializable when its graph has no cycle: there is some order in which each transaction saw only the ones before it. Each anomaly is a particular kind of cycle, or a read of data that should never have been seen.

The four cycle shapes. Solid arrows are dependencies (ww, wr) and dashed arrows are anti-dependencies (rw). G1a and G1b are not cycles: they are reads of a version that was rolled back, or that its writer overwrote before committing. G-cursor is the G-single shape on a single row, with write-dependencies where the read-dependency is.

Phenomenon	Adya's condition on the committed history	First level that forbids it
G0 write cycle	A cycle made only of `ww` edges	PL-1
G1a aborted read	A committed transaction read a version written by one that aborted	PL-2 (read committed)
G1b intermediate read	A committed transaction read a version that its writer later overwrote itself	PL-2
G1c circular information flow	A cycle made only of `ww` and `wr` edges	PL-2
G-cursor lost update	On a single item, a cycle of one `rw` edge and `ww` edges	PL-CS (cursor stability)
G-single read skew	A cycle with exactly one `rw` edge	PL-2+ (and snapshot isolation)
G2-item write skew	A cycle with one or more item `rw` edges	PL-2.99 (repeatable read)
G2 anti-dependency cycle	A cycle with one or more `rw` edges, including ones from `WHERE` clauses (phantoms)	PL-3 (serializable)

The difference between G-single and G2 is the number of anti-dependencies, and the two are easy to confuse. The textbook write skew (two on-call doctors who each see the other still on call and both go home) closes its cycle with two rw edges. That makes it G2, not G-single.

Where PostgreSQL's four levels sit

PostgreSQL level	Rules out	Still allows
`READ UNCOMMITTED`	Accepted, but runs exactly as `READ COMMITTED`
`READ COMMITTED`, this app	G0, G1a, G1b, G1c	G-cursor*, G-single, G2-item, G2
`REPEATABLE READ` (snapshot isolation)	…plus G-cursor and G-single	G2-item, G2
`SERIALIZABLE` (SSI)	All of them, by aborting a transaction with `40001`	None

* A lost update at READ COMMITTED needs the read and the write in separate statements. A single UPDATE … WHERE that has to wait for a row lock re-evaluates its WHERE clause against the row that was just committed, so it cannot overwrite a change it did not see. That is the whole of the G-cursor defence below.

Why each one cannot happen here

These are the anomalies in the script's order, which is Adya's order: weakest level first. Seat labels are the ones the script picks on a fresh 40-seat hall.

G0 Write cycle (dirty write)

Definition: Two transactions each overwrite something the other wrote, so the final state mixes both. T1 writes x and T2 overwrites it, while T2 writes y and T1 overwrites that.
At the cinema: Two couples book the same pair at the same moment, one clicking left to right and the other right to left. Each goes home with one seat of the pair.
The probe: Four holds, A3+A4 and A4+A3 twice each, released at the same instant on four separate connections, three rounds. It checks that exactly one order has both seats, that the others have neither, and that the seat map shows each seat taken once.
Why not here: A claim on a seat is a write. PostgreSQL never lets two transactions hold uncommitted writes to the same row or the same pending constraint entry: the second one waits until the first commits or rolls back. That is how writes work at every level, not an isolation setting. On top of that, a hold is all-or-nothing. BookingService.holdInternal inserts seat by seat under a SAVEPOINT. On a 23P01 it rolls back to the savepoint, withdraws the seats it already inserted, marks the order failed, and commits that record, so no hold ever commits part of a pair. Every hold also opens with SELECT … FOR UPDATE on the showing row, so holds on one showing run one at a time.
Made to happen in: Nowhere. There is no PostgreSQL setting under which it can occur.

G1a Aborted read

Definition: A transaction reads a version written by a transaction that then aborts.
At the cinema: The seat map shows a seat claimed by a booking that never went through.
The probe: 24 one-seat holds, on two lanes, on a seat the script already holds (A1). Each claim is written into the table, then rejected with 23P01 and undone by ROLLBACK TO SAVEPOINT, while three anonymous viewers read the seat map continuously. A read of a rolled-back claim would show A1 twice, because the seat map joins seats to their live claims. The probe checks that no read shows any seat twice.
Why not here: MVCC. A reader sees only versions whose transaction had committed when its statement began. A rolled-back version is invisible to everybody, forever. PostgreSQL has no dirty reads to switch on. The application adds its own version of the rule: seat-availability push notifications are sent only after a booking commits, so nobody is told about a change that could still roll back.
Made to happen in: Nowhere. PostgreSQL has no setting that permits it.

G1b Intermediate read

Definition: A transaction reads a version that its writer later overwrote before committing: a half-finished state.
At the cinema: During somebody's failed block booking, four seats flicker to "held" and back.
The probe: 24 holds of A8+A9+A10+B1+A1. The first four are written as held. Then A1, already taken, fails, and the four are rewritten cancelled before the transaction commits. Three viewers poll meanwhile. The probe checks that no read ever shows those four as taken, and that they are free afterwards.
Why not here: The same MVCC rule. Each row is read as of the last commit before the statement began, never as a version its writer replaced before committing. The held versions existed only inside the doomed transaction.
Made to happen in: Nowhere.

G1c Circular information flow

Definition: A cycle of dependencies with no anti-dependency in it: each transaction read something the other wrote.
At the cinema: Two couples reach for one pair from opposite ends. Each sees the other's half-made booking, both are told the seats are gone, and the pair goes unsold.
The probe: A5+A6 and A6+A5 at the same instant, three rounds. Each hold writes its first seat and then goes for the seat the other wrote first. For both to be refused, each must have read the other's uncommitted claim, which is a wr edge each way. The probe checks that exactly one of the two gets the pair every time, and never neither.
Why not here: A hold only ever meets someone else's claim through the EXCLUDE check, and PostgreSQL's check never acts on an uncommitted claim. It waits for the claiming transaction to commit or roll back, then decides. So one of the two always finds either nothing or a finished booking, and gets the pair. READ COMMITTED, PostgreSQL's floor, forbids G1c by definition. On one showing the two holds also queue on the showing's row lock, so the second does not even start until the first has finished.
Made to happen in: Nowhere.

G-cursor Lost update (ANSI P4)

Definition: Two transactions read the same row, and both write it based on what they read. The first write is silently overwritten.
At the cinema: A customer cancels a seat while the order is being confirmed, and the cancellation is swallowed: the seat stays sold. At the door, the same shape would let one barcode admit two people.
The probe: Hold B4+B5. Then confirm the order and cancel B4 within a few milliseconds of each other, six rounds. A lost update needs the cancel to commit inside the confirm's read-then-write window, and that window's width is unknown from outside the server. So instead of one fixed timing, the rounds sweep an offset of up to 20 ms either way: together; each side 20 ms ahead; each side 5 ms ahead; the confirm 10 ms ahead. Released exactly together, one side tends to win every time. The probe checks that B4 always ends cancelled, and that the order ends in one of the two states a serial order produces:
• confirm, then cancel: order confirmed, B5 confirmed;
• cancel, then confirm: the confirm is refused because a seat is no longer held, so the order stays pending and B5 stays held.
Why not here: READ COMMITTED does allow lost updates when an application reads in one statement and writes in the next. This app never does that. Each change is one conditional UPDATE:
• confirm is … WHERE status = 'held';
• cancel is … WHERE status IN ('held','confirmed');
• the admission scanner is … AND admitted_at IS NULL.
When two collide, the second waits for the first's row lock and then re-evaluates its WHERE clause against the row that was just committed. It cannot overwrite a change it did not see.
Made to happen in: Any read-then-write split over two statements. AdmissionRescanConcurrencyTest races eight scans of one ticket and asserts exactly one admission. The tree has no weakened twin of it that shows the double admission.

G-single Single anti-dependency cycle (read skew)

Definition: A reader sees part of the database from before a commit and part from after it: a state that never existed. The cycle has exactly one anti-dependency: the reader read x before the writer changed it, and read y after.
At the cinema: The seat map shows one seat of a two-seat order as held and the other as free.
The probe: Three rounds of: hold B2+B3, then confirm the order, while three viewers poll. It checks that every read shows the two seats in the same state. The script also reports how many reads saw them free, held and confirmed, which shows that the reads really did span both commits.
Why not here: READ COMMITTED does permit read skew, but only across statements. The seat map is one SQL statement (every seat left-joined to its live claim), and each statement reads one snapshot, so a commit is seen whole or not at all. Where a hold decides from several reads, it locks what it read: the showing FOR UPDATE, the seats FOR SHARE, and the customer FOR UPDATE.
Made to happen in: Reading the two seats with two statements at READ COMMITTED. The tree has no test for it.

Where read skew is still possible, and harmless: an order's own page reads the order and then its seats in two statements. A reload that lands exactly between them during a confirmation can show "pending" above seats that are already confirmed. That render decides nothing, and the next one is right.

G2-item Item anti-dependency cycle (write skew): the double booking

Definition: Two transactions each read something the other is about to change, and both act on what they read. That makes two anti-dependencies, one each way.
At the cinema: Two customers turn up with tickets for F7.
The probe: Eight holds on A7 at the same instant, three rounds, alternating between two accounts if you give it two. It checks that exactly one wins each round, that every loser is refused "just taken", and that the seat map shows the seat taken once.
Why not here: A booking that asked "is F7 free?" and then inserted a claim would be classic write skew. Both see the seat free and both claim it, and READ COMMITTED and REPEATABLE READ both let that through. This app never asks. A hold just inserts its claim, and
reservation_no_overlap EXCLUDE USING gist (resource_unit_id WITH =, period WITH &&) WHERE (status IN ('held','confirmed'))
rejects a second live claim on the same seat for an overlapping time at write time, the way a unique index would. It works at any isolation level and surfaces as 23P01, which is never retried. "Just taken" is the message that 23P01 path produces and nothing else produces, so every loser in the probe was refused by the constraint itself.
Made to happen in: SeatBookingConcurrencyDifferentialTest builds the schema from the real migration with the constraint stripped out, runs the same eight-way race, and all eight succeed. Note that it removes the constraint rather than weakening isolation, because there is no weaker isolation to go to.

A precise footnote. A claim is a new row, found by a predicate (this seat, an overlapping time, a live status), not a new version of an existing row. So in the "ask, then insert" version the read is a predicate read, and its cycle strictly meets Adya's G2 condition. The project's design notes file it under G2-item because it concerns one known seat. Either way, the constraint closes it by turning the predicate conflict into a write conflict on an index entry.

G2 Anti-dependency cycle over a predicate (phantom)

Definition: Each transaction's COUNT or WHERE clause would have come out differently had it seen the other's insert, and both act on their count.
At the cinema: One person with two tabs gets past the 10-seats-a-day limit. That limit exists for exactly this person: a scalper.
The probe: One account already holds 2 anchor seats that day. It sends two holds of 5 seats, on two showings of the same day, at the same instant. One hold fits (2 + 5 = 7). Both do not (2 + 5 + 5 = 12). The probe checks that one succeeds and the other is refused by the daily cap, whose message counts the first one's seats: "You already have 7 seats for showings on …, and the limit is 10 a day."
Why not here: The rows that would breach the cap do not exist yet, so there is nothing to lock. READ COMMITTED, and REPEATABLE READ too, would let both holds count 2 and both insert. So the hold locks the customer's own row, with SELECT … FOR UPDATE in CustomerRepository.findByIdForUpdate, before counting. That serialises one customer's holds and nothing else. SERIALIZABLE would also catch it, at the price of 40001 retries on every hold, and the lock does it at READ COMMITTED. The first-booking rule ("the first booking on a showing must be for at least 2 seats") is also a count, and it is serialised by the showing's FOR UPDATE.
Made to happen in: DailyPurchaseCapConcurrencyDifferentialTest runs four holds on four showings of one day, so that their showing locks do not overlap, with the customer lock left out. All four pass the count, and the day ends at 12 seats against a cap of 10. Its twin with the lock, DailyPurchaseCapConcurrencyTest, lets exactly three through. Like the other differential tests, it removes the protection rather than weakening isolation.

The race that is not an Adya anomaly

A booking reads the showing as on sale. Staff cancel the showing. The booking commits afterwards anyway. That is a ticket for a showing that had already been cancelled, the last row of the table. It has one anti-dependency and no edge back, so it is not a cycle. "Book, then cancel" is a perfectly valid serial order, and no isolation level objects, not even SERIALIZABLE. What is wrong is that the booking's check went stale before it committed: the cancellation committed in between. The business rule is that nothing may be sold once a cancellation has taken effect. That is a rule about when things commit, and serializability of any flavour, strict or not, says nothing about it for two transactions that overlap in time.

The fix is SELECT … FOR UPDATE on the showing row as every hold's first statement. Whichever of the two reaches the row first, the other waits, then reads the current status. SessionCancellationRaceDifferentialTest reverts it to a plain SELECT and gets the orphaned hold. The script does not probe it because cancelling a showing needs a staff account, and because it is not on Adya's list. It belongs on this page anyway: knowing where the taxonomy stops is part of knowing it.

Step by step: running the script

Check the tools. You need JDK 17 or newer (for jshell), bash, an env that understands -S (GNU coreutils 8.30+, or macOS/BSD), and network access to your deployment.
```
jshell --version        # jshell 17 or newer
env --version | head -1 # GNU coreutils 8.30 or newer (macOS: env -S is built in)
```
Download the script, and read it. It is one file of plain Java. It sends only what a customer's browser sends, and it cancels everything it books. Reading it before giving it your session cookie is the right instinct.
```
curl -fO https://dawud-tan.github.io/adya-anomaly-probe.jsh
chmod +x adya-anomaly-probe.jsh
less adya-anomaly-probe.jsh
```
Make two showings for it (staff). Signed in as staff on your deployment, open /admin, pick a hall of about 30 seats or more, and use Create showing twice:
- both on the same day, at least an hour from now, and not overlapping (for example 13:00–15:00 and 17:00–19:00);
- with a label such as Adya probe 1, and no film. A film with an age rating makes every hold record an age attestation for your account, and the script refuses such a showing.
A new showing is on sale immediately. Use fresh, empty ones: the script only ever touches free seats, but on an empty showing the final seat map shows at a glance that everything was given back.
Copy the two seat-map addresses. Open the hall's public page, https://<your-host>/halls/<hall-id>. The hall id is the one in the admin page's address. Press View seat map on each showing and copy the address bar. It looks like this:
```
https://<your-host>/halls/<hall-id>/showings/<showing-id>
```
Sign in as a customer. In a browser, open /login with an ordinary Google account. The platform-admin account cannot hold seats. Use one that has no other bookings on that day, because the daily cap counts them. The sign-in lasts about an hour, which is plenty; the run itself takes one or two minutes.
Copy the session cookie. Open developer tools (F12), go to Network, and reload. Click the first request (the page itself), then Headers, then Request Headers, then Cookie. Copy the whole value. The important part is q_session=…. A large session is split into q_session_chunk_1, _2 and so on, and copying the whole header takes them all. The cookie is HttpOnly, so document.cookie in the console will not show it. The script drops booking_lang by itself, because it reads the refusal messages in English.
Hand both to the script, keeping the cookie out of your shell history.
```
export ADYA_SHOWING='https://<your-host>/halls/…/showings/…'
export ADYA_SHOWING_2='https://<your-host>/halls/…/showings/…'
read -rs ADYA_COOKIE && export ADYA_COOKIE   # paste, then Enter; nothing is echoed
```
Settings are environment variables because jshell passes no arguments to a script. A cookie on a command line would also be visible to every user of the machine through ps.
Dry-run first. This reads the two seat maps and /orders, checks the rules and your session, prints the seat plan, and writes nothing:
```
ADYA_DRY_RUN=1 ./adya-anomaly-probe.jsh
```
Run it.
```
./adya-anomaly-probe.jsh; echo "exit status: $?"
```
To make the races between two people, sign in with a second Google account in a private window, copy its cookie the same way, and export ADYA_COOKIE_2. To run a subset: ADYA_ONLY=G0,G2-item ./adya-anomaly-probe.jsh.
Tidy up. The showing is empty again when the script ends; it prints the final seat map to prove it. Close or cancel the two probe showings in /admin so customers do not find them, and sign out at /logout. The cookie you copied stays a working credential until it expires, so treat the terminal it is in accordingly.

All settings

Variable		Meaning
`ADYA_SHOWING`	required	Seat-map address of an empty, on-sale, label-only showing at least an hour away
`ADYA_COOKIE`	required	Cookie header of a browser signed in as a customer (at least `q_session=…`; a bare value is taken to be `q_session`)
`ADYA_SHOWING_2`	optional	A second empty showing on the same day. Without it, G2's two holds also queue on one showing's lock (see limits)
`ADYA_COOKIE_2`	optional	A second customer, so every race alternates between two people
`ADYA_ONLY`	optional	Comma-separated subset: `G0,G1a,G1b,G1c,G-cursor,G-single,G2-item,G2` (`P4` also means G-cursor)
`ADYA_ROUNDS`	optional	Rounds per race, default 3, at most 10. G1a/G1b send 8 doomed holds per round, and G-cursor runs twice this many rounds
`ADYA_DRY_RUN`	optional	`1`: read-only preflight
`ADYA_NAME`, `ADYA_PHONE`	optional	Contact details sent with each hold. The app only stores them for an account that has never booked

Reading the output

Each probe prints what it did, round by round; one line on what it would look like at the cinema; a why not here paragraph; and a verdict:

NOT OBSERVED: every attempt ended the way a serial order would have ended.
OBSERVED: the anomaly happened. The script then exits with status 1.
INCONCLUSIVE: an attempt was refused for a reason other than the one being probed, such as a cap you had already reached, so the attempt says nothing.
SKIPPED: the probe does not apply. For example, G2 is skipped if the deployment has no daily cap, or if the two showings fall on different days.

Exit status: 0 no anomaly observed, 1 an anomaly observed, 2 could not run or not clean. For G1a, G1b and G-single the script also reports how many seat-map reads were in flight alongside a write that could have leaked. That count uses client-side timing, so it is an upper bound on how hard the window was actually tried.

Sample output: a full run against a local copy of the app

This run used the booking platform's own code on a local machine, with PostgreSQL 18.6 in a container and a test customer identity injected in place of the Google sign-in. There was no second account, and the two showings were on one day. A live run prints the same shape. Its counts and its duration differ, because every round trip to a remote server takes longer.

Adya anomaly probe -> http://localhost:8081
------------------------------------------------------------------------------
Showing   Test Showing | 2099-12-03 13:00 WIB | 40 seats, all free
          rules: 8 seats per booking, 10 per customer per day, first booking at least 2 seats
Showing 2 Test Showing | 2099-12-03 17:00 WIB | 40 seats, all free
          rules: 8 seats per booking, 10 per customer per day, first booking at least 2 seats
Accounts  customer 1: signed in (GET /orders -> 200)
Accounts  customer 2 not given: customer 1 plays both parts in every race.
Seats     A1+A2 anchor | A3+A4 G0 | A8+A9+A10+B1 G1b | A5+A6 G1c | B4+B5 G-cursor
          B2+B3 G-single | A7 G2-item | B6+B7+B8+B9+B10 + C1+C2+C3+C4+C5 (showing 2) G2
------------------------------------------------------------------------------

[anchor] seats held from the first probe to the last
   at the cinema: the showing is never empty, so the first-booking rule never refuses a one-seat hold
   A1+A2 held (order dfcfa9b8)

[G0] write cycle
   at the cinema: two couples book the same pair and each goes home with one seat of it
   round 1: A3+A4 and A4+A3, twice each, at once -> 1 of 4 succeeded, 3 refused, just taken; order e82da440 has A3 held, A4 held
   round 2: A3+A4 and A4+A3, twice each, at once -> 1 of 4 succeeded, 3 refused, just taken; order 97a701e7 has A3 held, A4 held
   round 3: A3+A4 and A4+A3, twice each, at once -> 1 of 4 succeeded, 3 refused, just taken; order 171e0bc7 has A3 held, A4 held
   => NOT OBSERVED: in all 3 rounds one order got both seats and the other three got neither

[G1a] aborted read
   at the cinema: the seat map shows a claim from a booking that never went through
   24 doomed one-seat holds on A1 (already held): each claim was written, then undone by ROLLBACK TO SAVEPOINT after 23P01 -> 24 refused, just taken
   26 seat-map reads meanwhile, 14 of them in flight alongside a doomed hold; a seat shown twice (or the grid changing size): 0x
   => NOT OBSERVED: 24 rolled-back claims, 26 reads (14 overlapping), none saw a claim that was rolled back

[G1b] intermediate read
   at the cinema: seats flicker to 'held' during someone's failed block booking
   24 doomed holds of A8+A9+A10+B1+A1: A8+A9+A10+B1 written as 'held', then A1 fails and they are rewritten 'cancelled' before commit
   28 seat-map reads meanwhile, 16 in flight alongside a doomed hold; A8+A9+A10+B1 seen held: 0x; all free afterwards: true
   => NOT OBSERVED: 24 doomed block holds, 28 reads (16 overlapping), no intermediate 'held' ever visible

[G1c] circular information flow
   at the cinema: two couples reach for one pair from opposite ends; each sees the other's half-made booking, both give up, and the pair goes unsold
   round 1: A5+A6 and A6+A5 at once -> 1 of 2 succeeded, 1 refused, just taken; order 12116a9d has A5 held, A6 held
   round 2: A5+A6 and A6+A5 at once -> 1 of 2 succeeded, 1 refused, just taken; order 263c7f98 has A5 held, A6 held
   round 3: A5+A6 and A6+A5 at once -> 1 of 2 succeeded, 1 refused, just taken; order e0d5ac26 has A6 held, A5 held
   => NOT OBSERVED: in all 3 rounds exactly one of the two got the pair; never neither

[G-cursor] lost update
   at the cinema: a customer cancels a seat and it stays sold anyway (each round: hold two seats, then confirm the order and cancel one of them within a few ms)
   round 1 (together): B4 cancelled, B5 confirmed, order confirmed  = confirm, then cancel
   round 2 (cancel 20 ms ahead): B4 cancelled, B5 held, order pending  = cancel, then confirm (refused: a seat was no longer held)
   round 3 (confirm 20 ms ahead): B4 cancelled, B5 confirmed, order confirmed  = confirm, then cancel
   round 4 (confirm 5 ms ahead): B4 cancelled, B5 confirmed, order confirmed  = confirm, then cancel
   round 5 (cancel 5 ms ahead): B4 cancelled, B5 confirmed, order confirmed  = confirm, then cancel
   round 6 (confirm 10 ms ahead): B4 cancelled, B5 confirmed, order confirmed  = confirm, then cancel
   => NOT OBSERVED: the cancel was never lost; every round matched a serial order {cancel, then confirm (refused: a seat was no longer held)=1, confirm, then cancel=5}

[G-single] single anti-dependency cycle
   at the cinema: the seat map shows half of somebody's two-seat order
   round 1: hold B2+B3, confirm, while 3 viewers poll -> 29 reads
   round 2: hold B2+B3, confirm, while 3 viewers poll -> 30 reads
   round 3: hold B2+B3, confirm, while 3 viewers poll -> 30 reads
   what the reads saw: both available x36, both confirmed x26, both held x27
   => NOT OBSERVED: 89 reads across 3 hold+confirm rounds; the pair was always in one state

[G2-item] item anti-dependency cycle
   at the cinema: two customers turn up with tickets for the same seat
   round 1: 8 holds on A7 at once -> 1 held it, 7 refused, just taken; the seat map shows it taken 1x
   round 2: 8 holds on A7 at once -> 1 held it, 7 refused, just taken; the seat map shows it taken 1x
   round 3: 8 holds on A7 at once -> 1 held it, 7 refused, just taken; the seat map shows it taken 1x
   => NOT OBSERVED: 24 simultaneous holds, exactly one winner in each of 3 rounds; every other one refused, just taken

[G2] anti-dependency cycle over a predicate
   at the cinema: one customer with two tabs gets past the 10-seats-a-day limit
   customer 1 already holds 2 seats that day; two holds of 5 at once -> refused by the daily cap | held (order 2b2c1fce)
   the refusal: "You already have 7 seats for showings on Thu 3 Dec, and the limit is 10 a day. You can add 3 more — untick 2 and try again."
   => NOT OBSERVED: one hold of 5 succeeded; the other was refused by the daily cap, having counted the first one's seats

[anchor] A1+A2 given back.

==============================================================================
Showing 1 after the run: every seat free again.
  G0        Write cycle (dirty write)                          NOT OBSERVED
  G1a       Aborted read                                       NOT OBSERVED
  G1b       Intermediate read                                  NOT OBSERVED
  G1c       Circular information flow                          NOT OBSERVED
  G-cursor  Lost update (P4)                                   NOT OBSERVED
  G-single  Single anti-dependency cycle (read skew)           NOT OBSERVED
  G2-item   Item anti-dependency cycle (double booking)        NOT OBSERVED
  G2        Anti-dependency cycle over a predicate (phantom)   NOT OBSERVED
  8 probe(s) ran; no anomaly was observed.
  151 writes (POST) and 255 reads (GET) in 12 s.
  Not probed: a showing cancelled mid-checkout. It is not an Adya anomaly (one
  anti-dependency edge, no cycle) and needs a staff account; see the guide.

Verbatim, except that each probe's "why not here" paragraph is left out; the cards above quote them.

What a run leaves behind, and its load

Seats. Every hold the script makes, it cancels again. The final seat map is printed to prove it. If a run is interrupted, a hold expires by itself within 10 minutes. A confirmed seat (the G-single and G-cursor probes confirm some) does not expire, so cancel anything left over at /orders. The script prints each order's id as it goes.
History. Your account's order history keeps the probe's cancelled and failed orders, and the tenant's audit log keeps a row for every change. Both are append-only by design; the audit log is a hash chain, and it is meant to be impossible to tidy up. Run it on a demo tenant, not on a cinema's live catalogue.
Load. A default run sends about 150 writes and a few hundred reads over a minute or two; the script prints the exact counts at the end. Most reads go to the seat-map fragment, the endpoint every open seat-map tab already polls every three seconds. The three seat-map viewers pause 100 ms between reads, and only watch while a probe is writing. This is a correctness probe, not a load test, so keep ADYA_ROUNDS modest.
Notifications. Every hold, confirmation and cancellation that succeeds sends a seat-availability push to anyone watching that showing's seat map with notifications allowed. A run makes dozens of them, and they are not throttled. Keep the probe showings' seat maps closed in any browser where you have allowed notifications. The script's own viewers are anonymous and subscribe to nothing.
Identification. Every request carries User-Agent: adya-anomaly-probe/1 (jshell; +https://dawud-tan.github.io/adya-anomaly-probe.html), so an operator reading the logs can see what it was.

What a live probe can and cannot show

A probe shows absence in the attempts it made. It does not prove impossibility. The windows it aims at are milliseconds wide, and the reads that happen to land in them are a sample. What makes each anomaly impossible is the mechanism named in its card. The script's job is to show that behaviour on the real server, over the real network, with the real configuration, which no unit test can do.

On one showing, holds queue on the showing's row lock. So the races on one showing (G0, G1c, G2-item) exercise that lock as much as the constraint. The losers are still refused by the constraint itself: "just taken" is only ever produced by the 23P01 path. The lock decides the order they arrive in, and the constraint decides who gets the seat. A race between two phones is a demonstration. The proof is the differential test.
G2 needs two showings to mean what it says. With only ADYA_SHOWING, both holds also queue on that showing's lock, and the per-customer lock is never the only thing between them.
One customer by default. Without ADYA_COOKIE_2, "two customers" are two connections of one account. The constraint does not care who asks. With a second account, the races are between two people.
Not covered: the counter channel, QRIS payments, the admission scanner and seat-map relayouts. Each needs staff credentials or money. They have their own tests in the repository (SeatRetirementRaceTest for relayouts, AdmissionRescanConcurrencyTest for the scanner).

Troubleshooting

You see	Why	Do
`illegal character: '#'`	You ran `jshell adya-anomaly-probe.jsh`; jshell does not skip a `#!` line	Run `./adya-anomaly-probe.jsh`. The error is harmless otherwise: the rest still runs
`env: invalid option -- 'S'`	An `env` older than coreutils 8.30	`tail -n +2 adya-anomaly-probe.jsh > probe.jsh && jshell probe.jsh`
`NoClassDefFoundError: java/net/http/HttpClient`	jshell was started with `--execution local`	Leave that flag off
`cookie is not a live session … sign-in at accounts.google.com`	The sign-in is over (about an hour), or the wrong cookie was copied	Sign in again and copy the whole `Cookie` header again
`may not book seats (HTTP 403)`	A platform-admin account	Use an ordinary Google account
`the showing is not on sale`	Closed, cancelled or still scheduled	Open it for sale in `/admin`, or make a new one
`film carries an age rating`	The showing has a rated film	Make a label-only showing
`showing starts at … at least an hour away`	Too soon: an under-sold showing is cancelled 15 minutes after its start	Use a later showing
`daily limit is already used up`	The account already has seats that day	Another day, or another account
`the hall is too small for the plan`	Fewer than about 30 free seats	A bigger hall, or fewer probes with `ADYA_ONLY`
G2 `SKIPPED … cannot race`	The two showings are on different days	Put both on the same day