Effective Stateless Model Checking for C/C++ Concurrency
Effective Stateless Model Checking for C/C++ Concurrency
复制标题
DOI：
10.1145/3158105
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Vafeiadis, Viktor
中科院分区：
文献类型：
--
作者：
Kokologiannakis, Michalis;Lahav, Ori;Vafeiadis, Viktor
我们提出了一个无状态模型检查算法，以验证RC11下运行的并发程序，RC11是C/C ++ 11内存模型的修复版本，而无需依赖性周期。与以前的大多数方法不同，该方法将线程交织到Sonic Partial订单减少的改进，我们的方法直接用于执行图，并且（在没有RMW指令和SC Atomics的情况下）避免了构造冗余探索。我们基于这种方法实现了一个称为RCMC的模型检查器，并将其应用于许多具有挑战性的并发程序。我们的实验证实，RCMC明显更快，比例比其他模型检查工具更好，并且对基准的小变化也更具弹性。
We present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C/C++11 memory model without dependency cycles. Unlike most previous approaches, which enumerate thread interleavings up to sonic partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and applied it to a number of challenging concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools, and is also more resilient to small changes in the benchmarks.