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。给定数据存储应用的一个可观测的可串行化执行轨迹，Isopredict生成并求解SMT约束，以发现该应用的一个可行执行中的不可串行化行为。Isopredict引入了创新技术来处理应用程序的差异行为；求解互递归约束集；并在覆盖率、精确性和性能之间取得平衡。在四个事务性数据存储基准上的评估表明，Isopredict通常能预测出不可串行化行为，其中99%的行为是可行的。