一句话：首个面向弱隔离数据存储应用的动态预测分析，通过SMT求解预测可行的不可串行化执行。
分布式数据存储通常提供弱隔离级别，虽高效但可能引入难以理解和调试的不可串行化行为。本文提出 IsoPredict，这是首个针对弱隔离级别下数据存储应用的动态预测分析。给定一次观测到的可串行化执行，IsoPredict 生成并求解 SMT 约束，以寻找该应用中可能发生且实际可行的不可串行化执行。为应对应用行为发散、互相递归的约束集以及覆盖、精度与性能之间的平衡，论文提出了若干新技术。作者在四个事务性数据存储基准上进行了评估，结果表明 IsoPredict 经常能预测出不可串行化行为，且其中 99% 的执行是实际可行的。
Distributed data stores typically provide weak isolation levels, which are efficient but can lead to unserializable behaviors, which are hard for programmers to understand and often result in errors. 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.
@article{paperbot2519,
title = {IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications},
author = {Chujun Geng and Spyros Blanas and Michael D. Bond and Yang Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656391}
}