Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications

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

TL;DR

IsoPredict tackles the challenge of uncovering unserializable executions in weakly isolated data stores by performing dynamic predictive analysis. It encodes feasible and unserializable executions as SMT constraints, offering exact and approximate approaches, including a rank-based anti-dependency framework to avoid circular reasoning. The method includes an optional validation step to replay predicted histories and verify feasibility under causal or read-committed isolation, reporting both predictive results and visualizations. Empirical evaluation across multiple benchmarks shows IsoPredict can predict feasible unserializable behaviors with high accuracy and reasonable performance, often matching MonkeyDB’s effectiveness while avoiding its reliance on bespoke data-store behavior. Overall, IsoPredict provides a principled, SMT-based mechanism to anticipate and diagnose weak-isolation anomalies from observed traces, enabling developers to debug and harden distributed data-store applications.

Abstract

This paper presents the first dynamic predictive analysis for data store applications under weak isolation levels, called Isopredict. Given an observed serializable execution of a data store application, Isopredict generates and solves SMT constraints to find an unserializable execution that is a feasible execution of the application. Isopredict introduces novel techniques that handle divergent application behavior; solve mutually recursive sets of constraints; and balance coverage, precision, and performance. An evaluation on four transactional data store benchmarks shows that Isopredict often predicts unserializable behaviors, 99% of which are feasible.

IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications

TL;DR

IsoPredict tackles the challenge of uncovering unserializable executions in weakly isolated data stores by performing dynamic predictive analysis. It encodes feasible and unserializable executions as SMT constraints, offering exact and approximate approaches, including a rank-based anti-dependency framework to avoid circular reasoning. The method includes an optional validation step to replay predicted histories and verify feasibility under causal or read-committed isolation, reporting both predictive results and visualizations. Empirical evaluation across multiple benchmarks shows IsoPredict can predict feasible unserializable behaviors with high accuracy and reasonable performance, often matching MonkeyDB’s effectiveness while avoiding its reliance on bespoke data-store behavior. Overall, IsoPredict provides a principled, SMT-based mechanism to anticipate and diagnose weak-isolation anomalies from observed traces, enabling developers to debug and harden distributed data-store applications.

Abstract

This paper presents the first dynamic predictive analysis for data store applications under weak isolation levels, called Isopredict. Given an observed serializable execution of a data store application, Isopredict generates and solves SMT constraints to find an unserializable execution that is a feasible execution of the application. Isopredict introduces novel techniques that handle divergent application behavior; solve mutually recursive sets of constraints; and balance coverage, precision, and performance. An evaluation on four transactional data store benchmarks shows that Isopredict often predicts unserializable behaviors, 99% of which are feasible.
Paper Structure (38 sections, 50 equations, 9 figures, 6 tables, 3 algorithms)

This paper contains 38 sections, 50 equations, 9 figures, 6 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Weakly Isolated Execution Histories
  4. Serializablility
  5. Causal Consistency
  6. Read Committed
  7. IsoPredict Overview
  8. Predictive Analysis
  9. Encoding of Feasible Execution
  10. Encoding Unserializability
  11. Constraints that encode an exact condition
  12. Constraints encoding a sufficient but unnecessary condition
  13. Adding anti-dependency order ($\mathit{rw}$) to $\mathit{pco}$
  14. Circular dependency and rank
  15. Generated constraints
  16. ...and 23 more sections

Figures (9)

  • Figure 1: Different executions of two sessions (clients) concurrently on the same account.
  • Figure 2: A causal, serializable history corresponding to Figure \ref{['fig:motivating_serial']}.
  • Figure 4: IsoPredict's components and workflow.
  • Figure 5: Including anti-dependency ordering ($\mathit{rw}$; dashed arrows) in $\mathit{pco}$ makes $\mathit{pco}$ cyclic.
  • Figure 6: An example of circular dependency: $\mathit{ww}\xspace(t_1, t_2)$ depends on $\mathit{pco}\xspace(t_1, t_3)$, which in turn depends on $\mathit{ww}\xspace(t_1, t_2)$.
  • ...and 4 more figures