IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
<|reference_start|>IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications: 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.<|reference_end|>
@article{geng2024isopredict:,
    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={Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 161.
  Publication date: June 2024},
    year={2024},
    doi={10.1145/3656391},
    archivePrefix={arXiv},
    eprint={2404.04621},
    primaryClass={cs.PL cs.DB}
}