IsoCheck
A black-box transactional isolation checker with a C++20 checking engine and Python workload harness that infers dependency graphs and detects isolation anomalies from client-observed histories.
Project overview
IsoCheck is a high-performance black-box transactional isolation checker implemented in C++20 with a Python 3.12 workload harness and an in-browser WebAssembly playground. It observes concurrent database operations purely from the client perspective, reconstructs per-key version orders, synthesizes directed dependency graphs, and identifies isolation anomalies via cycle search.
The problem: Verifying isolation without lock-table access
Modern distributed and relational databases frequently advertise ACID transactional isolation levels such as Read Committed, Repeatable Read, or Serializable. However, race conditions, edge-case lock acquisitions, and distributed consensus optimizations often introduce silent isolation bugs under concurrent load.
Traditionally, verifying isolation required white-box inspection: auditing internal lock tables, parsing write-ahead logs (WAL), or instrumenting the database kernel. In managed cloud environments, database users do not have administrative server access. IsoCheck solves this by inferring isolation anomalies purely from client-observable read and write histories.
System architecture & pipeline
Executes concurrent transactional clients using list-append micro-operations against target databases (PostgreSQL, CockroachDB).
Extracts client-observed invocation and completion timestamps, transaction IDs, read results, and committed write sets.
Infers the serialization sequence for each individual key by analyzing client-observed list extensions and prefix relationships.
Synthesizes directed edges: write-to-read (wr) when a transaction reads another's write, and write-to-write (ww) from version orders.
Runs Tarjan's Strongly Connected Components (SCC) and minimal cycle search to isolate dependency cycles and produce proof witnesses.
Compiles the full C++20 checking engine into WebAssembly, enabling zero-install, zero-cloud verification directly in the browser.
Checked isolation anomalies
Write Cycles (Dirty Write)
Two or more transactions overwrite shared keys in conflicting orders, violating total write order.
Aborted Reads
A transaction reads a version produced by a transaction that subsequently aborted or rolled back.
Circular Information Flow
Transactions exhibit circular dependencies in their read-write relationships (T1 reads from T2 while T2 reads from T1).
Unwritten Version Reads
A transaction observes a data version that was never committed by any transaction in the history.
Theoretical foundation & explicit limitations
IsoCheck grounds its checking logic directly in the formalisms of Atul Adya's generalized isolation theory (1999) and Elle (Kingsbury & Alvaro, 2020). By using list-append registers where every written value is unique, the checker can establish total version orders per key without ambiguous overwrites.
Explicit Black-Box Limitations
- Unobserved Internal States: Transactions aborted before the client receives an acknowledgment cannot be reconstructed unless their intermediate writes leak to concurrent reads.
- Predicate-Level Anomalies: Phantom reads and predicate locks cannot be verified without observing the database catalog schema or range scans.
- Clock Skew in Timelines: Client-side invocation/completion ordering requires synchronized client clocks or monotonic local counters to prevent false timeline waterflow drift.
Technical architecture & tools
- Checking Engine: C++20 (GCC 14 / Clang 18, CMake)
- Web Playground: WebAssembly via Emscripten, Cloudflare Pages
- Workload Harness: Python 3.12, AsyncIO, psycopg3
- Graph Algorithms: Tarjan's Strongly Connected Components (SCC), Johnson's cycle search
- Verified Targets: PostgreSQL 17.2, SQLite 3, CockroachDB