EXPERIMENT 04 / BUSINESS INVARIANT
Both committed. Nobody stayed.
Two doctors each leave only if another remains. A transaction can commit successfully and still participate in a business-rule violation.
Saved real MySQL 8.4 execution. The browser does not run SQL. This fixed-roster example makes no claim about range inserts, arbitrary existing snapshots, or performance.
Invariant: SUM(on_call) ≥ 1. Initial state (1,1); two withdrawal requests. The independent Python oracle enumerates both serial request orders and allows only (0,1) or (1,0). MySQL final rows are read separately after both participants commit.
Measured run JSON · Stop/start repeat JSON · Lifecycle & negative-control evidence · Editable SQL
Predict before reading the results
- Both counts finish before any write. Does a row-local AND on_call=1 condition protect the cross-row rule?
- Both create an RR snapshot first, then take an exclusive guard. Will the next plain count be fresh?
- Take the guard before the first consistent read, or read the roster FOR UPDATE. Which evidence must show B waited?
Measured outcomes, first repetition
| Isolation | strategy | A count | B count | Remaining | Serially reachable |
|---|---|---|---|---|---|
| READ COMMITTED | unguarded | 2 | 2 | 0 | NO |
| READ COMMITTED | late_guard | 2 | 1 | 1 | yes |
| READ COMMITTED | guard_first | 2 | 1 | 1 | yes |
| READ COMMITTED | locking_roster | 2 | 1 | 1 | yes |
| REPEATABLE READ | unguarded | 2 | 2 | 0 | NO |
| REPEATABLE READ | late_guard | 2 | 2 | 0 | NO |
| REPEATABLE READ | guard_first | 2 | 1 | 1 | yes |
| REPEATABLE READ | locking_roster | 2 | 1 | 1 | yes |
All rows above contain two successful commits. Approval is a separate decision. Each run repeats the matrix three times and swaps doctor IDs in repetition 2; the repeat follows a server stop/start. Timing is recorded only for ordering evidence, not a benchmark.
What changed, and why
- unguarded:Both read 2 before either writes. Distinct-row conditional updates both commit; (0,0) is a counterexample under RC and RR.
- late_guard:The lock really serializes access, but it cannot replace an existing RR read view. The follower still reads 2 under RR. Under RC its next statement reads 1 in this schedule.
- guard_first:No consistent read precedes the guard. B waits; its first count after A commits reads 1. Every writer must obey this protocol.
- locking_roster:A current locking read protects the rows used by the decision. B waits and then returns one active doctor. We test fixed membership, not all range/predicate cases.
Run, change SQL, rerun
python lab.py doctor
python lab.py start
python lab.py oncall --output .local/oncall-first.json
python lab.py stop
python lab.py start
python lab.py oncall --output .local/oncall-repeat.json
python scripts/validate_oncall.py .local/oncall-first.json .local/oncall-repeat.json
cp sql/oncall.json .local/oncall-sql.json
# Edit .local/oncall-sql.json, preserve the baseline
python lab.py oncall --sql-file .local/oncall-sql.json --output .local/oncall-edited.json
python lab.py stop- Baseline: explain the two disallowed terminal states before changing SQL. Read the bindings to confirm which doctor each actor changed.
- Equivalent rewrite: replace the count SQL with SELECT COALESCE(SUM(on_call),0) AS n FROM oncall_roster WHERE shift_id=1. Rerun the complete matrix; the semantics should match for the fixed roster.
- Negative control: remove FOR UPDATE from the guard query. The required B→A edge disappears and the runner must fail within its deadline without writing a success JSON. This rejects an invalid schedule assumption; it is not a new final-state proof.
- Explain why moving a plain read above guard_first recreates late_guard. Use the existing late_guard RR record as the counterexample, then compare RC.
Inspect actual evidence
READ COMMITTED / unguarded / remaining 0
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 0
}
],
"oracle": {
"on_call_count": 0,
"invariant_holds": false,
"serially_reachable": false,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"B": {
"doctor_id": 2,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
}
}
}No lock wait is claimed here. Both completed reads form the barrier.
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 18.576,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 2,
"elapsed_ms": 19.559,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 3,
"elapsed_ms": 19.568,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 20.126,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 20.131,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 6,
"elapsed_ms": 21.032,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 7,
"elapsed_ms": 21.035,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 21.464,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 21.471,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 10,
"elapsed_ms": 22.647,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 11,
"elapsed_ms": 22.651,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 12,
"elapsed_ms": 23.208,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 13,
"elapsed_ms": 23.211,
"actor": "coordinator",
"action": "barrier: both initial counts completed before writes"
},
{
"step": 14,
"elapsed_ms": 23.303,
"actor": "B",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
2
]
},
{
"step": 15,
"elapsed_ms": 23.328,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 16,
"elapsed_ms": 24.057,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 17,
"elapsed_ms": 24.06,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 18,
"elapsed_ms": 24.084,
"actor": "B",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
2
]
},
{
"step": 19,
"elapsed_ms": 24.087,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 20,
"elapsed_ms": 25.498,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 21,
"elapsed_ms": 25.822,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]READ COMMITTED / late_guard / remaining 1
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 1
}
],
"oracle": {
"on_call_count": 1,
"invariant_holds": true,
"serially_reachable": true,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 1,
"approved": false,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_guard | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_guard | None | IX | GRANTED |
| B | oncall_guard | PRIMARY | X,REC_NOT_GAP | WAITING |
| B | oncall_guard | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 7.396,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 2,
"elapsed_ms": 8.127,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 3,
"elapsed_ms": 8.132,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 8.746,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 8.748,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 6,
"elapsed_ms": 9.344,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 7,
"elapsed_ms": 9.346,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 9.865,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 9.872,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 10,
"elapsed_ms": 10.602,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 11,
"elapsed_ms": 10.606,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 12,
"elapsed_ms": 11.234,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 13,
"elapsed_ms": 11.237,
"actor": "coordinator",
"action": "barrier: both initial counts completed before writes"
},
{
"step": 14,
"elapsed_ms": 11.238,
"actor": "A",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 15,
"elapsed_ms": 11.903,
"actor": "A",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 16,
"elapsed_ms": 11.996,
"actor": "B",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 17,
"elapsed_ms": 25.861,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 18,
"elapsed_ms": 25.872,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 19,
"elapsed_ms": 25.876,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 20,
"elapsed_ms": 26.724,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 21,
"elapsed_ms": 26.729,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 22,
"elapsed_ms": 27.703,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 23,
"elapsed_ms": 27.706,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 24,
"elapsed_ms": 29.426,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 25,
"elapsed_ms": 29.495,
"actor": "B",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 26,
"elapsed_ms": 29.501,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 27,
"elapsed_ms": 30.322,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 1
}
]
},
{
"step": 28,
"elapsed_ms": 30.325,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 29,
"elapsed_ms": 31.188,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]READ COMMITTED / guard_first / remaining 1
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 1
}
],
"oracle": {
"on_call_count": 1,
"invariant_holds": true,
"serially_reachable": true,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 1,
"approved": false,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_guard | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_guard | None | IX | GRANTED |
| B | oncall_guard | PRIMARY | X,REC_NOT_GAP | WAITING |
| B | oncall_guard | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 9.927,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 2,
"elapsed_ms": 11.009,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 3,
"elapsed_ms": 11.013,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 11.621,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 11.63,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 6,
"elapsed_ms": 12.229,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 7,
"elapsed_ms": 12.232,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 12.835,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 12.84,
"actor": "A",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 10,
"elapsed_ms": 13.554,
"actor": "A",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 11,
"elapsed_ms": 13.663,
"actor": "B",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 12,
"elapsed_ms": 15.733,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 13,
"elapsed_ms": 15.737,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 14,
"elapsed_ms": 15.74,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 15,
"elapsed_ms": 16.691,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 16,
"elapsed_ms": 16.696,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 17,
"elapsed_ms": 17.423,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 18,
"elapsed_ms": 17.428,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 19,
"elapsed_ms": 18.986,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 20,
"elapsed_ms": 19.068,
"actor": "B",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 21,
"elapsed_ms": 19.091,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 22,
"elapsed_ms": 19.963,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 1
}
]
},
{
"step": 23,
"elapsed_ms": 19.967,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 24,
"elapsed_ms": 20.487,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]READ COMMITTED / locking_roster / remaining 1
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 1
}
],
"oracle": {
"on_call_count": 1,
"invariant_holds": true,
"serially_reachable": true,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 1,
"approved": false,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_roster | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_roster | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_roster | None | IX | GRANTED |
| B | oncall_roster | PRIMARY | X,REC_NOT_GAP | WAITING |
| B | oncall_roster | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 10.083,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 2,
"elapsed_ms": 10.702,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 3,
"elapsed_ms": 10.71,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 11.24,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 11.244,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED"
},
{
"step": 6,
"elapsed_ms": 11.721,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL READ COMMITTED",
"rows": []
},
{
"step": 7,
"elapsed_ms": 11.725,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 12.125,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 12.129,
"actor": "A",
"action": "submit",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE"
},
{
"step": 10,
"elapsed_ms": 12.897,
"actor": "A",
"action": "returned",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE",
"rows": [
{
"doctor_id": 1
},
{
"doctor_id": 2
}
]
},
{
"step": 11,
"elapsed_ms": 12.996,
"actor": "B",
"action": "submit",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE"
},
{
"step": 12,
"elapsed_ms": 15.375,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 13,
"elapsed_ms": 15.381,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 14,
"elapsed_ms": 15.386,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 15,
"elapsed_ms": 15.947,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 16,
"elapsed_ms": 15.95,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 17,
"elapsed_ms": 17.832,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 18,
"elapsed_ms": 17.877,
"actor": "B",
"action": "returned",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE",
"rows": [
{
"doctor_id": 2
}
]
},
{
"step": 19,
"elapsed_ms": 17.88,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 20,
"elapsed_ms": 18.419,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]REPEATABLE READ / unguarded / remaining 0
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 0
}
],
"oracle": {
"on_call_count": 0,
"invariant_holds": false,
"serially_reachable": false,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 2,
"approved": true,
"outcome": "committed"
}
}
}No lock wait is claimed here. Both completed reads form the barrier.
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 10.685,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 2,
"elapsed_ms": 11.194,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 3,
"elapsed_ms": 11.198,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 11.938,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 11.94,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 6,
"elapsed_ms": 12.602,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 7,
"elapsed_ms": 12.605,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 13.091,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 13.095,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 10,
"elapsed_ms": 13.815,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 11,
"elapsed_ms": 13.818,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 12,
"elapsed_ms": 14.337,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 13,
"elapsed_ms": 14.339,
"actor": "coordinator",
"action": "barrier: both initial counts completed before writes"
},
{
"step": 14,
"elapsed_ms": 14.434,
"actor": "B",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
2
]
},
{
"step": 15,
"elapsed_ms": 14.466,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 16,
"elapsed_ms": 15.365,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 17,
"elapsed_ms": 15.368,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 18,
"elapsed_ms": 15.414,
"actor": "B",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
2
]
},
{
"step": 19,
"elapsed_ms": 15.424,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 20,
"elapsed_ms": 17.547,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 21,
"elapsed_ms": 18.433,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]REPEATABLE READ / late_guard / remaining 0
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 0
}
],
"oracle": {
"on_call_count": 0,
"invariant_holds": false,
"serially_reachable": false,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 2,
"approved": true,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_guard | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_guard | None | IX | GRANTED |
| B | oncall_guard | PRIMARY | X,REC_NOT_GAP | WAITING |
| B | oncall_guard | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 6.902,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 2,
"elapsed_ms": 7.487,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 3,
"elapsed_ms": 7.49,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 8.008,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 8.01,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 6,
"elapsed_ms": 8.545,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 7,
"elapsed_ms": 8.547,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 9.054,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 9.058,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 10,
"elapsed_ms": 9.794,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 11,
"elapsed_ms": 9.796,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 12,
"elapsed_ms": 10.817,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 13,
"elapsed_ms": 10.82,
"actor": "coordinator",
"action": "barrier: both initial counts completed before writes"
},
{
"step": 14,
"elapsed_ms": 10.822,
"actor": "A",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 15,
"elapsed_ms": 11.438,
"actor": "A",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 16,
"elapsed_ms": 11.53,
"actor": "B",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 17,
"elapsed_ms": 14.814,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 18,
"elapsed_ms": 14.819,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 19,
"elapsed_ms": 14.821,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 20,
"elapsed_ms": 16.029,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 21,
"elapsed_ms": 16.034,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 22,
"elapsed_ms": 17.838,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 23,
"elapsed_ms": 17.842,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 24,
"elapsed_ms": 19.769,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 25,
"elapsed_ms": 19.83,
"actor": "B",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 26,
"elapsed_ms": 19.837,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 27,
"elapsed_ms": 20.487,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 28,
"elapsed_ms": 20.49,
"actor": "B",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
2
]
},
{
"step": 29,
"elapsed_ms": 21.136,
"actor": "B",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
2
]
},
{
"step": 30,
"elapsed_ms": 21.138,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 31,
"elapsed_ms": 22.756,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]REPEATABLE READ / guard_first / remaining 1
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 1
}
],
"oracle": {
"on_call_count": 1,
"invariant_holds": true,
"serially_reachable": true,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 1,
"approved": false,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_guard | PRIMARY | X,REC_NOT_GAP | GRANTED |
| A | oncall_guard | None | IX | GRANTED |
| B | oncall_guard | PRIMARY | X,REC_NOT_GAP | WAITING |
| B | oncall_guard | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 7.752,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 2,
"elapsed_ms": 8.148,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 3,
"elapsed_ms": 8.15,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 8.564,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 8.566,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 6,
"elapsed_ms": 9.101,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 7,
"elapsed_ms": 9.104,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 9.499,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 9.502,
"actor": "A",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 10,
"elapsed_ms": 10.003,
"actor": "A",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 11,
"elapsed_ms": 10.101,
"actor": "B",
"action": "submit",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE"
},
{
"step": 12,
"elapsed_ms": 11.833,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 13,
"elapsed_ms": 11.836,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 14,
"elapsed_ms": 11.838,
"actor": "A",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 15,
"elapsed_ms": 12.365,
"actor": "A",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 2
}
]
},
{
"step": 16,
"elapsed_ms": 12.369,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 17,
"elapsed_ms": 12.953,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 18,
"elapsed_ms": 12.956,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 19,
"elapsed_ms": 14.716,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 20,
"elapsed_ms": 14.802,
"actor": "B",
"action": "returned",
"sql": "SELECT shift_id FROM oncall_guard WHERE shift_id=1 FOR UPDATE",
"rows": [
{
"shift_id": 1
}
]
},
{
"step": 21,
"elapsed_ms": 14.81,
"actor": "B",
"action": "submit",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1"
},
{
"step": 22,
"elapsed_ms": 15.634,
"actor": "B",
"action": "returned",
"sql": "SELECT COUNT(*) AS n FROM oncall_roster WHERE shift_id=1 AND on_call=1",
"rows": [
{
"n": 1
}
]
},
{
"step": 23,
"elapsed_ms": 15.639,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 24,
"elapsed_ms": 16.269,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]REPEATABLE READ / locking_roster / remaining 1
Independent final state / oracle
{
"final_rows": [
{
"doctor_id": 1,
"on_call": 0
},
{
"doctor_id": 2,
"on_call": 1
}
],
"oracle": {
"on_call_count": 1,
"invariant_holds": true,
"serially_reachable": true,
"allowed_serial_states": [
[
0,
1
],
[
1,
0
]
]
},
"decisions": {
"A": {
"doctor_id": 1,
"observed_count": 2,
"approved": true,
"outcome": "committed"
},
"B": {
"doctor_id": 2,
"observed_count": 1,
"approved": false,
"outcome": "committed"
}
}
}| actor | table | index | mode | status |
|---|---|---|---|---|
| A | oncall_roster | PRIMARY | X | GRANTED |
| A | oncall_roster | PRIMARY | X | GRANTED |
| A | oncall_roster | PRIMARY | X | GRANTED |
| A | oncall_roster | None | IX | GRANTED |
| B | oncall_roster | PRIMARY | X | WAITING |
| B | oncall_roster | None | IX | GRANTED |
Executed timeline, with SQL parameters
[
{
"step": 1,
"elapsed_ms": 6.286,
"actor": "A",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 2,
"elapsed_ms": 6.803,
"actor": "A",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 3,
"elapsed_ms": 6.807,
"actor": "A",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 4,
"elapsed_ms": 7.317,
"actor": "A",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 5,
"elapsed_ms": 7.323,
"actor": "B",
"action": "submit",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ"
},
{
"step": 6,
"elapsed_ms": 7.828,
"actor": "B",
"action": "returned",
"sql": "SET SESSION TRANSACTION ISOLATION LEVEL REPEATABLE READ",
"rows": []
},
{
"step": 7,
"elapsed_ms": 7.831,
"actor": "B",
"action": "submit",
"sql": "START TRANSACTION"
},
{
"step": 8,
"elapsed_ms": 8.385,
"actor": "B",
"action": "returned",
"sql": "START TRANSACTION",
"rows": []
},
{
"step": 9,
"elapsed_ms": 8.389,
"actor": "A",
"action": "submit",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE"
},
{
"step": 10,
"elapsed_ms": 9.232,
"actor": "A",
"action": "returned",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE",
"rows": [
{
"doctor_id": 1
},
{
"doctor_id": 2
}
]
},
{
"step": 11,
"elapsed_ms": 9.334,
"actor": "B",
"action": "submit",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE"
},
{
"step": 12,
"elapsed_ms": 11.487,
"actor": "observer",
"action": "barrier: observed lock wait",
"waiting": "B",
"blocking": "A"
},
{
"step": 13,
"elapsed_ms": 11.491,
"actor": "coordinator",
"action": "barrier: release A only after observed B→A wait"
},
{
"step": 14,
"elapsed_ms": 11.494,
"actor": "A",
"action": "submit",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"parameters": [
1
]
},
{
"step": 15,
"elapsed_ms": 12.197,
"actor": "A",
"action": "returned",
"sql": "UPDATE oncall_roster SET on_call=0 WHERE shift_id=1 AND doctor_id=%s AND on_call=1",
"rows": [],
"parameters": [
1
]
},
{
"step": 16,
"elapsed_ms": 12.201,
"actor": "A",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 17,
"elapsed_ms": 14.238,
"actor": "A",
"action": "returned",
"sql": "COMMIT",
"rows": []
},
{
"step": 18,
"elapsed_ms": 14.292,
"actor": "B",
"action": "returned",
"sql": "SELECT doctor_id FROM oncall_roster WHERE shift_id=1 AND on_call=1 ORDER BY doctor_id FOR UPDATE",
"rows": [
{
"doctor_id": 2
}
]
},
{
"step": 19,
"elapsed_ms": 14.296,
"actor": "B",
"action": "submit",
"sql": "COMMIT"
},
{
"step": 20,
"elapsed_ms": 14.759,
"actor": "B",
"action": "returned",
"sql": "COMMIT",
"rows": []
}
]Theory and implementation boundary
CMU/MIT explain schedules, 2PL and multi-versioning. This experiment verifies specific MySQL 8.4 statements with autocommit disabled via explicit START TRANSACTION. It does not establish that all InnoDB reads follow strict 2PL or that every RR history is serializable. No API key, model, vector plugin or external database is involved.
Lecture and reading mapping → · MySQL 8.4 consistent reads · MySQL 8.4 locking reads