Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search
Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search
复制标题
预测可串行性违规：基于 SMT 的搜索与基于 DPOR 的搜索
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Aarti Gupta
中科院分区：
文献类型：
--
作者：
Arnab Sinha;S. Malik;Chao Wang;Aarti Gupta
在我们最近的工作中，我们解决了使用预测分析在并发程序中检测可串行化违规的问题，在那里我们使用了基于图的方法从给定的测试执行中导出预测模型。基于使用动态偏序约简（DPOR）的无状态模型检查，显式地进行预测模型的探索，以检查执行中事件的交替交织。虽然这在某些基准上是有效的，但在其他示例中，显式枚举的代价太高。这促使我们使用SMT求解器基于符号探索来检查替代方案。在本文中，我们提出了一个基于SMT的编码检测我们的预测模型中的串行化违规。基于SMT的编码用于检测更简单的原子性违规（两个线程和一个变量）之前已经使用过，但据我们所知，我们的工作是第一次使用它们来检测任何数量的线程和变量的可串行化违规。我们还描述了我们的DPOR为基础的显式搜索和修剪的细节，并提出了一个实验评估比较两种搜索技术。当其中一个比另一个更高级上级时，这提供了对实例特征的一些洞察。然后，这些特征可以用于预测给定实例的首选技术。
In our recent work, we addressed the problem of detecting serializability violations in a concurrent program using predictive analysis, where we used a graph-based method to derive a predictive model from a given test execution. The exploration of the predictive model to check alternate interleavings of events in the execution was performed explicitly, based on stateless model checking using dynamic partial order reduction (DPOR). Although this was effective on some benchmarks, the explicit enumeration was too expensive on other examples. This motivated us to examine alternatives based on symbolic exploration using SMT solvers. In this paper, we propose an SMT-based encoding for detecting serializability violations in our predictive model. SMT-based encodings for detecting simpler atomicity violations (with two threads and a single variable) have been used before, but to our knowledge, our work is the first to use them for serializability violations with any number of threads and variables. We also describe details of our DPOR-based explicit search and pruning, and present an experimental evaluation comparing the two search techniques. This provides some insight into the characteristics of the instances when one of these is superior to the other. These characteristics can then be used to predict the preferred technique for a given instance.