IsoCheck: Black-Box Transactional Isolation Checker

🌐 Live Web Application: https://isocheck.pages.dev/
⚡ Interactive Playground: https://isocheck.pages.dev/#/playground

IsoCheck is a high-performance black-box transactional isolation checker implemented in C++20 with a Python 3.12 workload harness. It infers dependency graphs from client-observed transaction histories and detects isolation anomalies via strongly connected component (SCC) and minimal cycle search.

---

🚀 Quick User Guide: How to Use IsoCheck (Simple & Fast)

What does IsoCheck do? (In Plain English)

When multiple users or services update a database at the exact same millisecond, concurrent transactions can clash. If the database engine has concurrency or isolation bugs, updates can get silently overwritten (Dirty Writes), uncommitted edits can leak into reports (Dirty Reads), or transactions can see impossible circular states (Circular Flow).

IsoCheck checks whether your database actually kept its consistency promises. You don't need root access, database server logs, or lock tables—it works purely from client-side observations ("black box").

---

Method 1: Use the Live Web Playground (Zero Install, Runs in Your Browser)

👉 Try it right now: https://isocheck.pages.dev/#/playground

1. Open the link: Visit https://isocheck.pages.dev/#/playground.
2. Choose a sample history: Click any test button on the top bar:
   • Clean (Valid): A normal, serial history with no concurrency errors.
   • G0 (Write Cycle): Two transactions overwriting each other in conflicting order.
   • G1a (Aborted Read): A transaction reading data that was cancelled/rolled back.
   • G1c (Circular Flow): Circular information dependency across transactions.
   • Garbage Read: A read returning data that was never written.
3. Click "Run Check" (or press Ctrl + Enter):
   • The C++ checking engine compiles to WebAssembly and runs 100% inside your browser. Your data never leaves your computer!
4. Read the visual results:
   • Dependency Graph: Interactive graph where transactions are circles and dependencies are directed arrows. Any detected cycle glows in red!
   • Timeline Waterfall: See concurrent client processes side-by-side on a timeline.
   • Verdict Report: Clear VALID (green) or VIOLATIONS DETECTED (red) status with an exact proof witness.

---

Method 2: Test Your Own Live Database (PostgreSQL, CockroachDB, TiDB)

If you run a live database and want to test it:

1. Clone and build the CLI:

   git clone https://github.com/Afnan-0206/IsoCheck.git
   cd IsoCheck
   cmake -B build -DCMAKE_BUILD_TYPE=Release && cmake --build build -j

2. Run a test workload against PostgreSQL:

   python harness/run_campaign.py \
     --engine postgres \
     --isolation read_committed \
     --clients 8 \
     --txns-per-client 500 \
     --output my_run.jsonl

3. Inspect the results:
   • In your terminal: ./build/cli/isocheck --input my_run.jsonl
   • Or in your browser: Drag and drop my_run.jsonl directly into the Live Web Playground for an instant visual dependency graph!

---

1. Overview & Theoretical Foundation

IsoCheck builds directly upon the mathematical formalisms established in:

• Atul Adya (1999): Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions.
• Kyle Kingsbury & Peter Alvaro (2020): Elle: Inferring Isolation Anomalies from Experimental Observations (arXiv:2003.10554).

Rather than inspecting internal lock tables or write-ahead logs, IsoCheck observes client-side transaction executions using unique list-append micro-operations. From the resulting histories, it reconstructs per-key version orders, synthesizes dependency graphs ($\to_{ww}, \to_{wr}$), and searches for minimal cycle witnesses.

---

2. Architecture & System Flow

%% Generated by https://gitdiagram.com/afnan-0206/isocheck
flowchart TD

subgraph group_harness["Workload Harness"]
  node_generator["Workload Generator<br/>[workload.py]"]
  node_runner["History Runner<br/>[runner.py]"]
  node_postgres_client["PostgreSQL Harness<br/>[postgres.py]"]
  node_campaign["Acceptance Campaign<br/>[run_campaign.py]"]
  node_buggy_runner["Buggy Control Runner<br/>[buggy_runner.py]"]
end

subgraph group_analysis["History Analysis"]
  node_history["History Parsing<br/>[history.cpp]"]
  node_checker["Anomaly Checker<br/>[checker.cpp]"]
  node_version_order["Version Inference<br/>[version_order.cpp]"]
end

subgraph group_graph["Dependency Analysis"]
  node_dependency_graph["Graph Construction<br/>[checker.cpp]"]
  node_cycle_search["Cycle Search<br/>[graph.cpp]"]
end

subgraph group_results["Results"]
  node_cli["Checker CLI<br/>[main.cpp]"]
  node_report["Verdict Output<br/>[main.cpp]"]
end

node_operator(("Operator"))
node_postgres[("PostgreSQL")]

node_operator -->|"starts campaign"| node_campaign
node_operator -->|"runs workload"| node_runner
node_generator -->|"supplies templates"| node_runner
node_runner -->|"executes transactions"| node_postgres_client
node_postgres_client -->|"runs SQL"| node_postgres
node_runner -->|"invokes checker"| node_cli
node_campaign -->|"checks histories"| node_cli
node_campaign -.->|"runs workload"| node_runner
node_buggy_runner -->|"runs checker"| node_cli
node_cli -->|"parses history"| node_history
node_cli -->|"checks history"| node_checker
node_checker -->|"extracts transactions"| node_history
node_checker -->|"infers versions"| node_version_order
node_checker -->|"builds graph"| node_dependency_graph
node_checker -->|"finds cycles"| node_cycle_search
node_dependency_graph -->|"uses version orders"| node_version_order
node_cycle_search -->|"searches graph"| node_dependency_graph
node_checker -->|"returns verdict"| node_report
node_report -->|"shows result"| node_operator

click node_generator "https://github.com/afnan-0206/isocheck/blob/main/harness/workload.py"
click node_runner "https://github.com/afnan-0206/isocheck/blob/main/harness/runner.py"
click node_postgres_client "https://github.com/afnan-0206/isocheck/blob/main/harness/postgres.py"
click node_campaign "https://github.com/afnan-0206/isocheck/blob/main/harness/run_campaign.py"
click node_buggy_runner "https://github.com/afnan-0206/isocheck/blob/main/harness/buggy_runner.py"
click node_cli "https://github.com/afnan-0206/isocheck/blob/main/cli/main.cpp"
click node_history "https://github.com/afnan-0206/isocheck/blob/main/core/src/history.cpp"
click node_checker "https://github.com/afnan-0206/isocheck/blob/main/core/src/checker.cpp"
click node_version_order "https://github.com/afnan-0206/isocheck/blob/main/core/src/version_order.cpp"
click node_dependency_graph "https://github.com/afnan-0206/isocheck/blob/main/core/src/checker.cpp"
click node_cycle_search "https://github.com/afnan-0206/isocheck/blob/main/core/src/graph.cpp"
click node_report "https://github.com/afnan-0206/isocheck/blob/main/cli/main.cpp"

classDef toneNeutral fill:#f8fafc,stroke:#334155,stroke-width:1.5px,color:#0f172a
classDef toneBlue fill:#dbeafe,stroke:#2563eb,stroke-width:1.5px,color:#172554
classDef toneAmber fill:#fef3c7,stroke:#d97706,stroke-width:1.5px,color:#78350f
classDef toneMint fill:#dcfce7,stroke:#16a34a,stroke-width:1.5px,color:#14532d
classDef toneRose fill:#ffe4e6,stroke:#e11d48,stroke-width:1.5px,color:#881337
classDef toneIndigo fill:#e0e7ff,stroke:#4f46e5,stroke-width:1.5px,color:#312e81
classDef toneTeal fill:#ccfbf1,stroke:#0f766e,stroke-width:1.5px,color:#134e4a
class node_generator,node_runner,node_postgres_client,node_campaign,node_buggy_runner toneBlue
class node_history,node_checker,node_version_order,node_postgres toneAmber
class node_dependency_graph,node_cycle_search toneMint
class node_cli,node_report toneRose
class node_operator toneIndigo

Loading

---

3. Problem Statement & Key Principles

Traditional database tests check whether queries succeed or match point assertions. However, multi-client race conditions under weak isolation levels (e.g. Read Committed, Repeatable Read, Snapshot Isolation) frequently allow subtle, non-serializable interleavings without generating database errors.

IsoCheck treats the database as a pure black box:

1. Clients concurrently issue transactions composed of ordered list-append operations (append and read).
2. Every appended integer is globally unique (enabling exact $1:1$ mapping between values and writing transactions: "traceability").
3. Each read returns an ordered list of values observed so far on that key.
4. From the collection of reads, IsoCheck infers the per-key version order.
5. From the version orders, IsoCheck constructs the directed dependency graph ($\to_{ww}, \to_{wr}$).
6. Any directed cycle in this graph serves as a sound, minimal witness proving an isolation violation.

---

4. Supported Anomalies & Classification Matrix

Anomaly	Classification	Graph Pattern / Property	Explanation
G0	Dirty Write / Write Cycle	Directed cycle of pure $\to_{ww}$ edges	Two or more transactions overwrite each other's updates concurrently in conflicting orders.
G1a	Aborted Read	Read observes value from aborted transaction	A committed transaction observes data modified by a failed/aborted transaction.
G1b	Intermediate Read	Read observes non-final write of active transaction	A transaction reads a state installed mid-way through another transaction before that transaction finished.
G1c	Circular Information Flow	Directed cycle of $\to_{ww}$ and $\to_{wr}$ edges	A cycle in the serialization graph involving both writes and reads.
Garbage Read	Data Corruption	Value observed that was never written	A read returns an element never appended by any transaction in history.
Inconsistent Read	Version Inconsistency	Read is not a prefix of the longest read	A read observed an out-of-order, truncated, or incompatible version sequence.
Internal Inconsistency	Read-Your-Writes Violation	Intra-txn read misses prior intra-txn write	A single transaction fails to observe its own preceding write to the same key.

---

5. Verification Engine & Algorithms

• Iterative Tarjan's SCC: Strongly connected components are identified with an explicit, heap-allocated DFS stack to prevent call-stack overflows on histories with $10^5+$ transactions.
• BFS Shortest Cycle Search: Once an SCC is identified, Breadth-First Search traverses the component to extract the strictly shortest cycle witness.
• Per-Key Version Inference: Aggregates all reads per key, finds the longest compatible sequence, and establishes the ground-truth sequence of versions.
• Exact Witness Formatting: Emits compact, human-readable witness strings (e.g., T1 ->ww T2 ->wr T1) along with full JSON-structured output.

---

6. Workload Harness & Fault Injection

• Skewed Workload Generator (workload.py): Generates deterministic, seedable transaction templates with Zipfian key skew to induce high lock contention.
• Concurrent History Runner (runner.py): Spawns multiple worker threads issuing parallel transactions, recording precise wall-clock timestamps for :invoke and :ok/:fail events.
• PostgreSQL Harness (postgres.py): Uses PostgreSQL list-append tables (key VARCHAR, val INT[]) with atomic array appends (array_append) under configurable isolation levels (READ COMMITTED, REPEATABLE READ, SERIALIZABLE).
• Buggy Control Runner (buggy_runner.py): Injects intentional isolation faults (e.g., non-atomic multi-step appends or dirty reads) to validate checker sensitivity and verify positive detection.

---

7. Repository Structure

IsoCheck/
├── CMakeLists.txt              # Root build configuration (C++20, warnings, dependencies)
├── Dockerfile                  # Multi-stage container build (gcc:14 + slim runtime)
├── docker-compose.yml          # Containerized Postgres 17 + Toxiproxy + IsoCheck
├── cli/                        # isocheck CLI binary
│   ├── CMakeLists.txt
│   └── main.cpp
├── core/                       # Core static library
│   ├── include/isocheck/       # Public headers (history.h, version_order.h, graph.h, checker.h)
│   └── src/                    # Implementations (iterative Tarjan, BFS shortest cycle, inference)
├── harness/                    # Workload generation and database harness
│   ├── workload.py             # Skewed list-append generator with unique values
│   ├── postgres.py             # Postgres driver supporting RC, RR, Serializable
│   ├── runner.py               # Concurrent multi-client history recorder
│   ├── run_campaign.py         # Acceptance campaign runner
│   ├── buggy_runner.py         # Fault injection positive control runner
│   └── requirements.txt
├── tests/                      # Unit test suites and hand-crafted fixtures
│   ├── fixtures/               # JSONL test fixtures (positive & negative cases)
│   ├── core/                   # GoogleTest suites (history, version_order, graph, checker)
│   └── elle/                   # Differential testing suite against Jepsen Elle
└── docs/                       # Project documentation
    ├── ARCHITECTURE.md         # Invariants, components, and data flow
    ├── DESIGN_DECISIONS.md     # Rationale and tradeoffs
    ├── LIMITATIONS.md          # Transparent boundaries of black-box testing
    └── BENCHMARKS.md           # Controlled benchmark results & methodology

---

8. Building, Testing & CLI Usage

Prerequisites

• CMake $\ge 3.24$
• C++20 compliant compiler (g++ 14+, clang++ 16+)
• Ninja or Make build system
• Python 3.12+ with psycopg[binary]

Build

mkdir -p build && cd build
cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
ninja

Running Tests

# C++ GoogleTest suite
./build/tests/isocheck_tests

# Python workload unit tests
pytest tests/test_workload.py tests/test_elle_convert.py

CLI Execution

# Human-readable report
./build/cli/isocheck history.jsonl

# Machine-readable JSON output
./build/cli/isocheck --json history.jsonl

Web Application & In-Browser Playground

IsoCheck includes an in-browser WebAssembly-powered interactive documentation and testing playground:

cd website
npm install
npm run dev

Open http://localhost:5173 to test transaction histories with real-time cycle visualization directly in your browser.

---

9. PostgreSQL Acceptance Campaign & Differential Testing

20-Seed Campaign

Execute the automated campaign across isolation levels:

python harness/run_campaign.py \
    --checker-bin ./build/cli/isocheck \
    --runs 20 \
    --clients 8 \
    --txns 65

Fault-Injected Positive Control

Verify detection sensitivity on buggy execution traces:

python harness/buggy_runner.py \
    --checker-bin ./build/cli/isocheck \
    --runs 20 \
    --isolation "READ COMMITTED"

Differential Testing with Elle

Histories are validated differentially against Jepsen's Clojure-based Elle engine (elle.list-append/check) using the tests/elle/ converter and runner to guarantee theoretical conformance.

---

10. Performance Benchmarks & Boundaries

Metric	Result	Environment
Peak Throughput	~142,000 txns/sec	AMD Ryzen / Intel Core, single thread
Graph Construction	$O(|V| + |E|)$ linear time	Adjacency lists with indexed lookup
Cycle Detection	Sub-millisecond on 10k ops	Tarjan SCC + BFS cycle recovery
Memory Footprint	$< 45\text{ MB}$ at $10^5$ events	Compact struct representation

Known Boundaries

• Black-box limits: Cannot detect anomalies when concurrent operations touch disjoint keys or when uncommitted transactions leave zero trace in observed reads.
• Prefix requirement: Relies on observable list-append prefix chains; unobserved intermediate states can only be flagged when reflected in read output.

---

License

MIT License. See LICENSE for details.