Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
复制标题
使用属性驱动修剪进行动态模型检查以检测竞争条件
DOI：
10.1007/978-3-540-88387-6_11
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
G. Gopalakrishnan
中科院分区：
文献类型：
--
作者：
Chao Wang;Yu Yang;Aarti Gupta;G. Gopalakrishnan
我们在动态模型检查中提出了一种新的属性驱动的修剪算法，以有效地检测多线程程序中的种族条件。主要思想是使用基于锁定的执行分析来帮助修剪动态搜索探索的搜索空间。我们假设无状态搜索算法用于系统地以深度优先的搜索顺序执行程序。如果我们的保守锁定分析表明搜索子空间是无种族空间的，则可以通过在深度优先搜索中避免回到某些州的回溯来修剪它。新的动态种族检测算法既声音又完整（与Flanagan和Godefroid的动态部分减少算法一样精确）。该算法在实践上也更有效，可以使其比实际的多线程C程序更好地扩展。
We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset based analysis of observed executions to help prune the search space to be explored by the dynamic search. We assume that a stateless search algorithm is used to systematically execute the program in a depth-first search order. If our conservative lockset analysis shows that a search subspace is race-free, it can be pruned away by avoiding backtracks to certain states in the depth-first search. The new dynamic race detection algorithm is both sound and complete (as precise as the dynamic partial order reduction algorithm by Flanagan and Godefroid). The algorithm is also more efficient in practice, allowing it to scale much better to real-world multithreaded C programs.