事务程序在因果一致性下的最佳无状态模型检查
摘要：高效的无状态模型检查（SMC）并发程序的框架在五个著名的因果一致性模型（CCv, CM, CC, 读提交和读原子）下进行。我们的方法是基于程序顺序（po）和读取关系（rf）之间的轨迹探索。我们的SMC算法在探索每个po和rf关系时是可证明最优的。我们在一个名为TRANCHECKER的工具中实现了我们的框架。实验结果表明，TRANCHECKER在检测经典分布式数据库基准测试中的异常方面表现良好。
作者：Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ashutosh Gupta, Shankaranarayanan Krishna, Omkar Tuppe
论文ID：2211.09020
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-01-18