Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Vbox: Efficient Black-Box Serializability Verification

Weihua Sun, Zhaonian Zou

TL;DR

Vbox presents a universal, black-box method for serializability verification that extends Cobra by supporting predicate operations, leveraging transaction time information, and adopting a simplified SAT formulation with a custom solver. It constructs a richer known graph, reduces constraints, and uses a compact transitive closure to achieve scalable, protocol-agnostic verification. Empirical results show Vbox detects more anomalies and runs significantly faster with lower memory than prior controllers, across real and synthetic workloads up to 100K transactions. The work advances practical, rigorous verification of serializable isolation in DBMS while remaining robust to different concurrency control protocols.

Abstract

Verifying the serializability of transaction histories is essential for users to know if the DBMS ensures the claimed serializable isolation level without potential bugs. Black-box serializability verification is a promising approach. Existing verification methods often have one or more limitations such as incomplete detection of data anomalies, long verification time, high memory usage, or dependence on specific concurrency control protocols. In this paper, a new black-box serializability verification method called \textsf{Vbox} is proposed. \textsf{Vbox} is powered by a number of new techniques, including the support for predicate database operations, comprehensive applications of transactions' time information in the verification process, and a simplified satisfiability (SAT) problem formulation and its efficient solver. In this paper, \textsf{Vbox} is verified to be correct, efficient, and capable of detecting more data anomalies, while not relying on any specific concurrency control protocols.

Vbox: Efficient Black-Box Serializability Verification

TL;DR

Vbox presents a universal, black-box method for serializability verification that extends Cobra by supporting predicate operations, leveraging transaction time information, and adopting a simplified SAT formulation with a custom solver. It constructs a richer known graph, reduces constraints, and uses a compact transitive closure to achieve scalable, protocol-agnostic verification. Empirical results show Vbox detects more anomalies and runs significantly faster with lower memory than prior controllers, across real and synthetic workloads up to 100K transactions. The work advances practical, rigorous verification of serializable isolation in DBMS while remaining robust to different concurrency control protocols.

Abstract

Verifying the serializability of transaction histories is essential for users to know if the DBMS ensures the claimed serializable isolation level without potential bugs. Black-box serializability verification is a promising approach. Existing verification methods often have one or more limitations such as incomplete detection of data anomalies, long verification time, high memory usage, or dependence on specific concurrency control protocols. In this paper, a new black-box serializability verification method called \textsf{Vbox} is proposed. \textsf{Vbox} is powered by a number of new techniques, including the support for predicate database operations, comprehensive applications of transactions' time information in the verification process, and a simplified satisfiability (SAT) problem formulation and its efficient solver. In this paper, \textsf{Vbox} is verified to be correct, efficient, and capable of detecting more data anomalies, while not relying on any specific concurrency control protocols.

Paper Structure

This paper contains 19 sections, 6 theorems, 10 equations, 9 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Black-box Serializability Verification
  4. Problem Statement
  5. Cobra: A Baseline Approach
  6. Limitations of Cobra
  7. Our Method Vbox
  8. Handling Predicate Operations
  9. Effective Construction of Known Graph
  10. Constraint Reduction
  11. Efficient Reachability Test
  12. Simplified SAT Problem Formulation
  13. Customized SAT Problem Solver
  14. Evaluation
  15. Completeness
  16. ...and 4 more sections

Key Result

theorem 1

A complete history of a set of transactions is serializable if and only if its DSG has no cycles, and there are neither aborted reads nor intermediate reads.

Figures (9)

  • Figure 1: An observed history.
  • Figure 2: Black-box serializability verification.
  • Figure 3: Compact transitive closure.
  • Figure 4: Updating transitive closure and path matrix.
  • Figure 5: Solve Example
  • ...and 4 more figures

Theorems & Definitions (9)

  • definition 1
  • definition 2
  • definition 3
  • theorem 1
  • theorem 2
  • theorem 3
  • theorem 4
  • lemma 1
  • lemma 2