Formal Theory & Mathematical Foundation

1. Formal Model of Transactions and Execution Schedules

ChaosSQL establishes its mathematical foundations upon classical database concurrency theory developed by Bernstein, Goodman, Papadimitriou, and Adya.

Formal Definition of a Transaction

A transaction T_i is formally defined as an ordered tuple:

T_i = (O_i, <_i)

Where:

• O_i is a finite set of atomic read operations r_i[x], write operations w_i[x], commit c_i, or abort a_i, accessing data items x ∈ D.
• <_i is a strict partial order over O_i reflecting the deterministic program flow of the transaction.
• There exists exactly one terminal operation t_i ∈ {a_i, c_i}, which is the maximal element under <_i.

Formal Definition of an Execution Schedule (History)

A concurrent execution schedule S over a finite set of transactions T = {T₁, T₂, …, T_n} is a partial order S = (bigcup_i=1ⁿ O_i, <_S) satisfying:

1. bigcup_i=1ⁿ <_i  ⊆  <_S (preserves the intra-transaction instruction ordering of each transaction).
2. For any two conflicting operations o_i, o_j ∈ S (where i ≠ j), either o_i <_S o_j or o_j <_S o_i.

2. Bernstein Conflict Conditions & CSR Theorem

Bernstein Conflict Condition (1966)

Two operations o_i, o_j ∈ S belonging to distinct transactions (i ≠ j) are in direct conflict if and only if they access the same data entity x ∈ D and at least one of them is a write mutation (w):

Conflict(o_i, o_j) ⟺ (target(o_i) = target(o_j) = x)  ∧  (o_i is w  ∨  o_j is w)

Direct Serialization Graph (Adya Dependency Graph)

Given an execution schedule S, the Direct Serialization Graph SG(S) = (V, E) is a directed graph where:

• Vertices V = T correspond to the set of committed transactions.
• A directed edge (T_i → T_j) ∈ E exists if and only if there exist o_i ∈ T_i and o_j ∈ T_j such that o_i <_S o_j and Conflict(o_i, o_j).

The Three Fundamental Dependency Relations (Atul Adya, 1999)

1. Read Dependency (wr): T_i  —^wr→  T_j if T_i writes a version of x and T_j subsequently reads that same version.
2. Overwrite Dependency (ww): T_i  —^ww→  T_j if T_i writes a version of x and T_j subsequently overwrites x.
3. Anti-Dependency (rw): T_i  —^rw→  T_j if T_i reads a version of x and T_j subsequently writes a newer version of x, invalidating the currency of T_i's read.

Fundamental Theorem of Conflict Serializability (CSR)

The existence of any directed cycle (T₁ → T₂ → … → T₁) proves that the execution is semantically inconsistent and possesses no equivalent serial ordering.

3. Probabilistic Concurrency Testing (PCT-SQL) (Burckhardt & Musuvathi)

Naive random concurrency testing fails due to combinatorial explosion. For n transactions executing m steps each, the total number of possible interleavings Ω grows factorially:

|Ω| = ((n · m)!)⁄(m!)ⁿ

For merely 5 transactions with 3 steps each, there exist 168,168,000 possible interleavings. The probability of hitting a critical context switch purely by chance is below 10^-6.

Burckhardt Lower Bound Theorem (ASPLOS 2010)

Burckhardt and Musuvathi proved that if a concurrency bug has a schedule depth d (the number of priority constraints or critical context switches required to trigger it), the Probabilistic Concurrency Testing (PCT) algorithm finds it in a single run with at least this probability:

ℙ(Detection) ≥ 1⁄(n · k^d-1)

Where n is the number of concurrent threads and k is the total number of executed steps.

Practical Application to Relational Databases

• Seminal empirical research (Lu et al., ASPLOS) demonstrates that ~96% of real-world concurrency bugs have depth d = 1 or d = 2 (Lost Update requires d=1; Write Skew requires d=2).
• For d = 2, the single-run detection probability is ℙ ≥ 1⁄(n · k). In a test with 4 workers and 25 steps (n=4, k=25), ℙ ≥ 1⁄100 = 1%.
• In a short batch of R = 300 runs:

ℙ(Find Bug in R Runs) = 1 - (1 - 1⁄100)³⁰⁰ ≈ 1 - e^-3 ≈ 95.02%

4. Minimization with Andreas Zeller Delta-Debugging (ddmin)

Formal Definition of 1-Minimality

Let C = ⟨ op₁, op₂, …, op_N ⟩ be the ordered sequence of scheduled operations that triggers an invariant failure test(C) = FAIL.

A subsequence C^* ⊆ C is defined as 1-Minimal if and only if:

test(C^*) = FAIL   ∧   ∀ op ∈ C^*: test(C^* ∖ {op}) = PASS

The ddmin Implementation in ChaosSQL

ChaosSQL replays each candidate subsequence against a freshly reset database and keeps it only when it reproduces the same failure signature: a violation status on the same invariant. A candidate that ends in a different status, such as an execution error from FOREIGN KEY constraint failed caused by removing the operation that created a parent row, does not count as a reproduction and is discarded.

1. Replays are memoized, so a subsequence already tested is never executed twice.
2. After ddmin converges, a final audit removes each remaining operation once and confirms that the failure disappears, which establishes 1-minimality.
3. The shrinker does not compute data dependencies between operations; it relies on the signature check to reject candidates that break referential integrity.

5. Linearizability and Black-Box Observations (Elle)

Inspired by the testing methodology of Kyle Kingsbury (Jepsen) and Peter Alvaro (VLDB 2020), ChaosSQL infers transactional anomalies strictly from client-observable operation histories (reads, writes, commits, and returns). No internal database engine instrumentation or custom storage bytecode is required, making ChaosSQL universally compatible with any SQL-compliant relational database.