Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AWDIT: An Optimal Weak Database Isolation Tester

Lasse Møldrup, Andreas Pavlogiannis

TL;DR

This work tackles the challenge of efficiently testing weak database isolation to detect anomalies in large-scale histories. It introduces AWDIT, an optimal tester that achieves $O(n^{3/2})$ time for RC and RA and $O(n\cdot k)$ for CC, backed by conditional lower bounds showing near-optimality. The authors prove general and per-level lower bounds under standard hypotheses, and demonstrate substantial practical speedups over state-of-the-art testers across multiple DBs and benchmarks. Empirical results show AWDIT outperforming baselines by orders of magnitude on large histories, with reliable anomaly witnesses and scalable performance. Overall, AWDIT provides a theoretically solid and practically impactful tool for validating weak isolation in modern distributed databases.

Abstract

In order to achieve low latency, high throughput, and partition tolerance, modern databases forgo strong transaction isolation for weak isolation guarantees. However, several production databases have been found to suffer from isolation bugs, breaking their data-consistency contract. Black-box testing is a prominent technique for detecting isolation bugs, by checking whether histories of database transactions adhere to a prescribed isolation level. Testing databases on realistic workloads of large size requires isolation testers to be as efficient as possible, a requirement that has initiated a study of the complexity of isolation testing. Although testing strong isolation has been known to be NP-complete, weak isolation levels were recently shown to be testable in polynomial time, which has propelled the scalability of testing tools. However, existing testers have a large polynomial complexity, restricting testing to workloads of only moderate size, which is not typical of large-scale databases. In this work, we develop AWDIT, a highly-efficient and provably optimal tester for weak database isolation. Given a history $H$ of size $n$ and $k$ sessions, AWDIT tests whether H satisfies the most common weak isolation levels of Read Committed (RC), Read Atomic (RA), and Causal Consistency (CC) in time $O(n^{3/2})$, $O(n^{3/2})$, and $O(n \cdot k)$, respectively, improving significantly over the state of the art. Moreover, we prove that AWDIT is essentially optimal, in the sense that there is a conditional lower bound of $n^{3/2}$ for any weak isolation level between RC and CC. Our experiments show that AWDIT is significantly faster than existing, highly optimized testers; e.g., for the $\sim$20% largest histories, AWDIT obtains an average speedup of $245\times$, $193\times$, and $62\times$ for RC, RA, and CC, respectively, over the best baseline.

AWDIT: An Optimal Weak Database Isolation Tester

TL;DR

This work tackles the challenge of efficiently testing weak database isolation to detect anomalies in large-scale histories. It introduces AWDIT, an optimal tester that achieves time for RC and RA and for CC, backed by conditional lower bounds showing near-optimality. The authors prove general and per-level lower bounds under standard hypotheses, and demonstrate substantial practical speedups over state-of-the-art testers across multiple DBs and benchmarks. Empirical results show AWDIT outperforming baselines by orders of magnitude on large histories, with reliable anomaly witnesses and scalable performance. Overall, AWDIT provides a theoretically solid and practically impactful tool for validating weak isolation in modern distributed databases.

Abstract

In order to achieve low latency, high throughput, and partition tolerance, modern databases forgo strong transaction isolation for weak isolation guarantees. However, several production databases have been found to suffer from isolation bugs, breaking their data-consistency contract. Black-box testing is a prominent technique for detecting isolation bugs, by checking whether histories of database transactions adhere to a prescribed isolation level. Testing databases on realistic workloads of large size requires isolation testers to be as efficient as possible, a requirement that has initiated a study of the complexity of isolation testing. Although testing strong isolation has been known to be NP-complete, weak isolation levels were recently shown to be testable in polynomial time, which has propelled the scalability of testing tools. However, existing testers have a large polynomial complexity, restricting testing to workloads of only moderate size, which is not typical of large-scale databases. In this work, we develop AWDIT, a highly-efficient and provably optimal tester for weak database isolation. Given a history of size and sessions, AWDIT tests whether H satisfies the most common weak isolation levels of Read Committed (RC), Read Atomic (RA), and Causal Consistency (CC) in time , , and , respectively, improving significantly over the state of the art. Moreover, we prove that AWDIT is essentially optimal, in the sense that there is a conditional lower bound of for any weak isolation level between RC and CC. Our experiments show that AWDIT is significantly faster than existing, highly optimized testers; e.g., for the 20% largest histories, AWDIT obtains an average speedup of , , and for RC, RA, and CC, respectively, over the best baseline.

Paper Structure

This paper contains 24 sections, 27 theorems, 5 equations, 9 figures, 1 table, 4 algorithms.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Our Contributions
  4. Preliminaries
  5. Definitions
  6. Weak Isolation Levels
  7. Weak Isolation Algorithms
  8. Read Committed
  9. Read Atomic
  10. Causal Consistency
  11. Witnesses of Reported Violations
  12. Complexity Lower Bounds
  13. A General Lower Bound for Weak Isolation Testing
  14. Lower Bounds with One and Two Sessions
  15. Implementation and Experiments
  16. ...and 9 more sections

Key Result

theorem 1

Given a history $H$ of size $n$, checking whether $H$ satisfies $\mathsf{RC}$ or $\mathsf{RA}$ can be decided in $O(n^{3/2})$ time.

Figures (9)

  • Figure 1: An $\mathsf{RC}$-inconsistent history (\ref{['subfig:intro_rc']}) and a $\mathsf{CC}$-inconsistent history (\ref{['subfig:intro_cc']}). $\operatorname{AWDIT}$ infers a small set of partial commit edges ${\color{CO}\mathsf{co}}'$ that are sufficient to witness the inconsistency in each case and identify small witnesses by means of simple cycles. Inferred ${\color{CO}\mathsf{co}}'$ edges that go along ${\color{SO}\mathsf{so}}\cup {\color{WR}\mathsf{wr}}$ are not shown explicitly.
  • Figure 2: Examples of violations of the five axioms of Read Consistency.
  • Figure 3: The axioms of Read Committed (\ref{['subfig:isolation-levels-rc']}), Read Atomic (\ref{['subfig:isolation-levels-ra']}), and Causal Consistency (\ref{['subfig:isolation-levels-cc']}). In each case, the ${\color{CO}\mathsf{co}}$ ordering is required when the other orderings hold.
  • Figure 4: Examples of consistent histories that violate consistency of stronger isolation levels.
  • Figure 5: The history $H$ given an undirected graph $G$. Using the semantics of $\mathsf{RC}$ (\ref{['subfig:isolation-levels-cc']}), we derive $t_3^{\mathrm{W}}\xrightarrow{{\color{CO}\mathsf{co}}}t_2^{\mathrm{W}}$ and $t_2^{\mathrm{W}}\xrightarrow{{\color{CO}\mathsf{co}}}t_3^{\mathrm{W}}$, implying that $H$ does not satisfy $\mathsf{RC}$, indicating that $G$ has a triangle.
  • ...and 4 more figures

Theorems & Definitions (34)

  • theorem 1
  • theorem 2
  • theorem 3
  • theorem 4
  • theorem 5
  • theorem 6
  • definition 1
  • definition 2
  • definition 3: Read Consistency
  • definition 4: Read Committed
  • ...and 24 more