PaperlayerView exact revision on arXiv

Source-linked AI summary

Augur: Predicting View Serializability Violations in Relational Data Store Applications

Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, Yang Wang

arXiv:2609.05288v1cs.PL

TL;DR

Weak isolation enables scalable data-store applications but permits unserializable behaviors, while prior predictive analyses mishandle relational SQL and can report non-View-Serializable executions. Augur models supported SQL queries symbolically and predicts feasible executions that violate View Serializability. The evaluation finds such executions in OLTP-Bench programs and all five Spree benchmarks.

  • Problem

    Weak isolation permits unserializable behaviors, while prior predictive analyses mishandle relational SQL and report executions that do not violate View Serializability.

  • Method

    Augur symbolically models supported SQL queries and iteratively identifies feasible executions that satisfy weak isolation and violate View Serializability.

  • Results

    Augur finds feasible, unserializable executions in OLTP-Bench programs and all five Spree benchmarks.

  • Takeaways & Limitations

    Augur provides a practical, data-store-agnostic analysis for detecting View Serializability violations in real SQL-based applications.

  • Takeaways & Limitations

    Spree evaluation excludes unsupported multi-table outer joins, subqueries, and certain multi-table inner joins because they accessed read-only tables in the analyzed executions.

Abstract

from arXiv · show

Data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation to achieve scalable performance, resulting in sporadic unserializable executions that are incorrect or fail. Prior work uses dynamic predictive analysis to infer violations from execution traces, but it cannot handle relational (i.e., SQL) queries with complex predicates, and it predicts executions that do not violate View Serializability. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in the widely used OLTP-Bench programs and in the widely used e-commerce application Spree.

1 Introduction

Weak isolation improves performance but permits difficult-to-detect unserializable behaviors, while prior predictive analyses mishandle SQL queries and View Serializability. Augur addresses these limitations by modeling relational queries and precisely predicting feasible violations, with evaluation on benchmarks and Spree.

  • Motivation: Weak isolation improves scalability but permits unserializable behaviors that can cause serious errors in real systems.Such behaviors may emerge unexpectedly under heavy load, high contention, or other unusual conditions.
  • Motivation: Dynamic predictive analysis can explore feasible unserializable executions from observed executions without requiring application source code.It checks a set of executions while avoiding the precision and scalability pitfalls of static analysis and model checking.
  • Prior limitations: Prior predictive analyses treat SQL queries as executed reads and writes, causing false negatives and false positives.They also predict executions that do not violate View Serializability.
  • Challenges: Modeling SQL predicates requires constraints for predicate matching, conditional responses, and conditional updates, while View Unserializability requires a new solution beyond polynomial-size quantifier-free SMT constraints.View Serializability requires every write–read ordering consistent with the predicted trace to be unserializable.
  • Augur: Augur generates SMT constraints that model supported SQL behavior and iteratively rules out equivalent history classes to find feasible View Serializability violations.Its constraints account for changed reads, writes, matched rows, and subsequent query responses.
  • Augur and evaluation: Augur is data-store agnostic, conservatively accounts for application-level dependencies, and targets executions feasible under correctly implemented weak isolation.The evaluation compares Augur with IsoPredict and examines OLTP-Bench programs and Spree.

3 Modeling Executions of Data Store Applications

Augur models data-store executions through observable SQL statement–response traces and distinguishes traces from dependency-explicit histories. This framework supports relational queries and defines View Serializability precisely, avoiding false positives from histories that generate serializable traces.

  • SQL semantics: Augur targets a SQL subset including SELECT, INSERT, UPDATE, and DELETE statements with predicates, INNER JOIN, SUM, and COUNT.Its statements follow SQL-standard behavior subject to stated simplifying assumptions.
  • SQL semantics: SELECT, UPDATE, and DELETE conceptually read every row because nonmatching rows implicitly contribute predicate information.This semantics captures how changing unseen row values can change which rows match a query.
  • Execution traces: An execution trace records transactions, session order, and each statement’s data-store response at the application–data store boundary.Responses are multisets of tuples for SELECT and affected-row counts for data-changing statements.
  • Execution histories: An execution history adds write–read dependencies to the same transactions and session order, making intertransaction dependencies explicit.The View function interprets histories and determines the responses they generate.
  • Execution histories: Multiple histories can generate the same trace because different writers may leave query responses unchanged, so trace-level reasoning must account for all generating histories.A serializable and an unserializable history may therefore be observationally identical.
  • Isolation levels: A trace satisfies an isolation level if at least one history generating it satisfies that level, while Augur ensures predicted traces have no serializable generating history.This existential trace definition supports precise View Serializability checking.

4 Design

Augur predicts feasible, unserializable executions from an observed trace by encoding SQL behavior, dependencies, weak-isolation constraints, and history feasibility in SMT. It then checks predicted histories and traces to target View Serializability violations.

  • Augur observes application–data store interactions and predicts a feasible, unserializable history from the resulting execution trace.The observed execution need not be serializable, although predicting from an unserializable observed trace is trivial.
  • Its two main technical contributions encode complex SQL query semantics and precisely filter predictions for View Serializability violations.The SQL encoding symbolically computes divergent queries and transactional dependencies; the trace-checking method iterates until it finds an unserializable trace.
  • Predictive constraint generation builds an SMT model from the observed trace to find a predictable history satisfying feasibility, the target weak isolation level, and unserializability.The encoding uses quantifier-free first-order logic over uninterpreted functions and linear integer arithmetic.
  • The model represents predicted write–read ordering and read values with functions over statements and accessed rows.Undefined function values are left unconstrained when a statement does not read a row or its transaction is excluded.
  • Augur encodes session order, write–read order, and their transitive happens-before closure as constraints used throughout prediction.These functions support the subsequent SQL, isolation-level, and unserializability constraints.

Encoding the predicted history.

The predicted history encoding fixes observed ordering while symbolically representing dependencies and SQL behavior. It converts SQL expressions to SMT expressions and constrains histories to remain feasible when predicted responses differ.

  • The encoding represents session order, write–read order, and happens-before relationships with SMT functions.Session-order constraints are generated for every distinct pair of observed transactions.
  • Feasibility constraints exclude transactions after statements whose predicted and observed responses differ.Different read values or writer transactions can change predicate matches, writes, and returned responses.
  • Augur converts SQL expressions and predicates into SMT expressions to model predicate-dependent writes and query responses.For mutating queries, responses are modeled as counts of rows matching the predicate.
  • Algorithm 2, SqlToSmt, maps literals and column names to symbolic values and recursively translates operators into SMT expressions.The design handles the queries recognized by the paper’s grammar, while constraints for LIMIT, COUNT, and SUM are omitted for brevity.
  • The encoding maintains consistency between predicted write–read dependencies and the values assigned to reads.These consistency constraints connect the dependency functions to the symbolic values used by SQL expressions.

Dependency–value consistency.

Augur computes values written by SQL statements from symbolic row values and SQL assignments, preserving consistency between dependencies and predicted data.

  • The helper function 𝜙wrval derives a writer’s value for a row from its assignments and the row’s symbolic read values.Columns absent from an UPDATE assignment retain values from 𝜙rdval(w)(row); INSERT and DELETE receive special treatment.

Identifying divergent statements .

Augur identifies divergent statements by comparing predicted and observed responses, enforces the target weak isolation level, and searches for cyclic partial commit orders. A serializable-trace checker filters histories whose views are serializable, while the analysis is argued sound and complete up to its PCO approximation.

  • Identifying divergent statements: Augur marks writing statements divergent when their predicted matching-row count differs from the observed response.For SELECT statements, divergence compares the predicted multiset response with the observed multiset.
  • Identifying divergent statements: For SELECTs, Augur symbolically evaluates predicates and selected values across rows, including joined rows for INNER JOIN queries.Joined-row values combine disjoint attribute sets before evaluating the select list, join condition, and predicate.
  • Identifying divergent statements: Transactions occurring after divergent statements are excluded from the predicted execution.The divergence variables generate constraints that enforce this exclusion.
  • Encoding the Weak Isolation Level: For target weak isolation level L, Augur requires a total commit order consistent with happens-before and L’s arbitration order.The encoding uses an integer-valued commit-order function to represent the total order.
  • Encoding the Weak Isolation Level: Augur supports additional framework-defined weak isolation levels, including Snapshot Isolation, but does not establish whether other levels can be encoded.This is an explicit scope boundary of the isolation-level encoding.
  • Encoding Unserializability: A cyclic partial commit order is used as a sufficient condition for an unserializable history, although such a history may still generate a serializable trace.The partial order combines dependency relations and excludes transactions removed after divergent statements.
  • Checking View Serializability: The serializable-trace checker tests whether any serializable history has the predicted history’s view and rules out that view when one exists.Augur repeats prediction with constraints forbidding previously checked views until it finds an unserializable trace or no further history.
  • Checking View Serializability: Few iterations are required in practice because each added constraint removes an equivalence class of histories sharing a view.The approach excludes a predicted view rather than only one predicted history.

5 Implementation

Augur is implemented as a transparent MySQL proxy that records application–data store interactions without requiring application changes.

  • Implementation: The inline monitor relays queries and responses between the application and a MySQL backend as a transparent proxy.Applications can use the monitor without modification.
  • Implementation: The monitor records per-session traces containing queries, responses, and the data store’s initial state.Sessions may connect to one shared monitor instance or separate instances.

SQL parser and PCG.

Augur’s SQL parser converts queries and responses into structures for predictive constraint generation, while PCG constructs and solves SMT constraints through Z3Py.

  • SQL parser and PCG: The SQL parser and predictive constraint generation support all query types specified in Fig. 3.The parser converts SQL queries and responses into data structures usable by PCG.
  • SQL parser and PCG: SQL values are mapped to integers, including assigning unique integer IDs to distinct strings, to simplify SMT conversion.This conversion lets the constraint generator operate over integer representations.
  • SQL parser and PCG: PCG uses Z3Py to construct, assert, and solve constraints, extending IsoPredict while reducing redundant SMT constraints.The implementation represents SMT functions as uninterpreted Z3 functions for better performance.
  • Evaluation questions: The evaluation asks whether SQL modeling improves coverage or precision, whether View Serializability prediction improves precision, and how effective and performant Augur is.Experiments use benchmark applications and a real data store backend.
  • Experimental setup: Experiments used Intel Xeon nodes with 192 GB of RAM, Python 3.12, Z3 4.15.4.0, and MySQL 8.0.43.These are the reported experimental software and hardware settings.

Common methodology.

The comparative evaluation contrasts Augur with IsoPredict under controlled workloads, showing that SQL-aware modeling avoids false negatives while trace-level prediction avoids false positives.

  • Comparative setup: Augur is compared directly with IsoPredict using IsoPredict’s custom data store backend.The comparison targets Causal and Read Committed isolation levels.
  • Comparative limitations: The comparison is limited because IsoPredict requires a custom backend and supports only simple key–value queries.Consequently, only four OLTP-Bench programs are included and most queries match single rows.
  • View Serializability: IsoPredict produces false positives when predicted unserializable histories generate serializable traces, while Augur reports only unserializable traces by design.Voter has no such discrepancies because its workload offers no two histories with the same trace.
  • SQL modeling: Augur’s SQL modeling exposes false negatives that IsoPredict misses when UPDATE queries combine reads with conditional writes.IsoPredict’s read/write decomposition can exclude the write from a predicted trace, whereas Augur models the full UPDATE.
  • Performance: Augur generates and solves constraints faster than IsoPredict across benchmarks and configurations, enabling the large-workload evaluation.The speedup is attributed to eliminating redundancy in generated constraints.
  • MySQL evaluation: Augur effectively finds predictable unserializable traces under Repeatable Read, but Wikipedia has 8 of 10 observed traces without predictions because seven are read-only.The search generally concludes in 1.0–1.2 average iterations, while solving time varies substantially with configuration.

Methodology.

The Spree evaluation tests request-level isolation on checkout workloads and finds feasible violations across all five benchmarks, while scalability becomes limited for large traces.

  • Spree methodology: Spree evaluation uses MySQL with Repeatable Read, the database’s default isolation level, on checkout-focused HTTP workloads.Checkout was selected because it involves race-condition reports, many SQL transactions, and relatively many writes.
  • Spree methodology: The five benchmarks model checkout interactions such as adding items before or after checkout completion.Their serializable behaviors specify the expected ordering of these operations.
  • Spree methodology: The inline monitor records only requests relevant to concurrent behavior, excluding initialization operations.The infrastructure submits HTTP requests that Spree translates into SQL queries sent to MySQL.
  • Scalability methodology: The scalability benchmark varies n sessions and m requests per session, executing n×m requests that add items to a shared cart.The serial behavior is that all n×m items are added.
  • Isolation model: Augur evaluates Spree at request-level isolation because each HTTP request should appear atomic despite spanning multiple SQL transactions.The study reports three repetitions per benchmark, with average timing variation below 2%.
  • SQL scope: Unsupported queries with multiple INNER JOINs, OUTER JOINs, or subqueries are ignored because they access only read-only tables in these executions.This is a workload-specific safety condition, not unrestricted parser support.
  • Spree results: Augur predicts feasible unserializable behavior for all five Spree programs, and manual inspection verifies that each prediction violates the benchmark’s serializable behavior.Strict and relaxed modes perform similarly, with consistently few prediction iterations.
  • Scalability results: Assertions and constraint-generation time grow roughly quadratically with workload size, while solving time grows faster.Solving depends on sessions, transactions, and statements because these affect serializability and divergence computations.

A SMT Constraints for the Strict Prediction Mode

Strict prediction mode extends Augur’s SMT formulation to control which SQL-statement dependencies participate in cycle searches and to constrain predicted responses. These constraints cover writes, reads, and inner joins.

  • Dependency exclusion: Strict prediction assigns each SQL statement an indicator for whether its dependencies should participate in cycle searching.The indicator extends 𝜙excluded(T) with statement-level Boolean values.
  • Dependency exclusion: Predictive constraint generation excludes a statement from a pco cycle when its transaction is excluded or an earlier statement diverges from the observed execution.
  • Response matching: After serializable solving iterations, PCG constrains Boolean mismatch variables to compare predicted and observed statement responses.For writes, mismatch counts predicate-true rows; for SELECTs, it compares predicted and symbolic multisets.
  • Response matching: For SELECT statements with INNER JOIN, PCG compares predicted responses against combinations of rows from both joined tables using the select list, join condition, and predicate.

C Full Experimental Results

The full-results section reports Augur’s OLTP-Bench and Spree evaluations through tables covering effectiveness, performance, workloads, and isolation settings.

  • OLTP-Bench: Table 6 reports full OLTP-Bench results, extending earlier results with the small workload.
  • Spree: Table 7 reports full Spree benchmark results, extending earlier results with Read Committed.
  • Evaluation setup: Table 6 evaluates Augur under Repeatable Read with MySQL, averaging results across 10 runs.Average assertions and execution times are rounded to three significant digits.
  • Evaluation setup: Table 7 summarizes Augur’s effectiveness and performance on Spree, excluding ignored statements from statement counts.Average assertions and execution times are rounded to three significant digits.
Loading 2609.05288v1…