Reordering control approaches to state explosion in model checking with memory consistency models
Reordering control approaches to state explosion in model checking with memory consistency models
复制标题
使用内存一致性模型进行模型检查中状态爆炸的重新排序控制方法
DOI：
10.1007/978-3-319-72308-2_11
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
and Toshiyuki Maeda
中科院分区：
文献类型：
--
作者：
Tatsuya Abe;Tomoharu Ugawa;and Toshiyuki Maeda
内存一致性模型的宽松性，允许指令及其效果的重新排序，加剧了软件模型检测的状态爆炸问题。在本文中，我们提出了三种方法，可以减少在软件模型检查与内存一致性模型访问的状态数。所提出的方法控制指令的重新排序。第一种方法控制重新排序的指令的数量。第二种方法预先指定要重新排序的指令，并防止其他指令被重新排序。第三种方法指定重新排序的指令，并优先探索具有重新排序的执行跟踪。我们应用这些方法的McSPIN模型检查器，我们一直在开发，并报告的有效性的方法，通过检查各种并发程序。
The relaxedness of memory consistency models, which allows the reordering of instructions and their effects, intensifies the state explosion problem of software model checking. In this paper, we propose three approaches that can reduce the number of states to be visited in software model checking with memory consistency models. The proposed methods control the reordering of instructions. The first approach controls the number of reordered instructions. The second approach specifies the instructions that are reordered in advance, and prevents the other instructions from being reordered. The third approach specifies the instructions that are reordered, and preferentially explores execution traces with the reorderings. We applied these approaches to the McSPIN model checker that we have been developing, and reported the effectiveness of the approaches by examining various concurrent programs.