论文标题
在因果一致性下对交易计划的最佳无状态模型检查
Optimal Stateless Model Checking of Transactional Programs under Causal Consistency
论文作者
论文摘要
我们提出了一个在因果一致性的五个突出模型，CCV，CM，CC的五个突出模型下的有效无状态模型检查（SMC）的框架。我们的方法基于探索程序顺序（PO）和（RF）关系的读取的痕迹。从某种意义上说，我们的SMC算法完全可以探索一次PO和RF关系。我们已经在称为Tranchecker的工具中实现了框架。实验表明，Tranchecker在检测古典分布式数据库基准中的杂菌方面表现良好。
We present a framework for efficient stateless model checking (SMC) of concurrent programs under five prominent models of causal consistency, CCv,CM,CC, Read Committed and Read Atomic. Our approach is based on exploring traces under the program order (po) and the reads from (rf) relations. Our SMC algorithm is provably optimal in the sense that it explores each po and rf relation exactly once. We have implemented our framework in a tool called TRANCHECKER. Experiments show that TRANCHECKER performs well in detecting anamolies in classical distributed databases benchmarks.
