Part 7 · 2 chapters · ~12 min

Theory You Will Actually Cite

Flat, nested and saga transaction models, isolation levels as anomaly definitions (ANSI versus Adya), why REPEATABLE READ means different things in Postgres, MySQL and Oracle, Jepsen's methodology and how to read a Jepsen report, and the capstone: a relational algebra interpreter and functional-dependency analyser.

13

Isolation and Jepsen

Transaction models: flat transactions are all-or-nothing; nested transactions let sub-transactions abort independently (savepoints are a limited form); sagas (Garcia-Molina and Salem, 1987) split a long transaction into steps with compensations, giving up isolation for availability (Workflows course P6).

Reading a Jepsen report: find the claimed guarantees (what the vendor documents), the workload (registers, bank transfers, append lists), the faults injected (partitions, clock skew, process pauses, crashes), and the anomalies found, named by Adya's phenomena (G-single, G2-item). Then check which versions and settings were affected and what was fixed. The bank workload, which checks that total balance never changes under concurrent transfers, is the test most relevant to fintech.

ISOLATION LEVELS, DEFINED BY ANOMALIES
Adya's phenomena versus vendor labels
G0 dirty writeOverwriting uncommitted data.Prevented by every level.G1 dirty readReading uncommitted or aborteddata. Prevented from ReadCommitted.lost updateRead-modify-write overwritten.Allowed at Read Committed.G2-item write skewAllowed by snapshot isolation;prevented by Serializable.G2 phantomPredicate reads change. Preventedby Serializable.vendor names"Repeatable Read" is SI inPostgres, locking in MySQL InnoDB,different again in others.
swipe the figure sideways, or tap expand for full screen
1/4
ANSI's problem
The SQL standard defined levels by three English phenomena. Berenson et al. (1995) showed the definitions were ambiguous and missed snapshot isolation entirely.
ambiguous standardBerenson et al. 1995
14

Capstone: an algebra interpreter and FD analyser

code
// the course capstone, ~80 lines of TypeScript (run with node, Node 23.6+ strips types)
// relational algebra: select, project, rename, union, diff, product, njoin, semijoin, antijoin, division
// FD analysis: closure, candidate keys (minimal superkeys over all subsets), BCNF violations
// concurrency: precedence graph and conflict-serialisability check

// real output
σ owner=Ada: [{"acct":"A1","owner":"Ada"}]
accounts ⋈ transfers: 3 rows
antijoin (accounts with none): [{"owner":"Chi"}]
division (accounts using every rail): [{"acct":"A1"}]
closure {A}: ABMO  closure {T}: ABMOT
candidate keys: [ 'T' ]
BCNF violations: [ 'A→OB', 'B→M' ]
SCP keys: [ 'CS', 'PS' ]  BCNF violations: [ 'P→C' ]
precedence edges: [ 'T1→T2', 'T2→T1' ]  conflict-serializable: false

// extensions: a 3NF synthesis algorithm from a minimal cover; a lossless-join test (chase);
// a tiny optimiser that pushes selections below joins and prints the rewritten expression