Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
复制标题
DOI：
10.1007/978-3-319-47677-3_8
复制
发表时间：
2016-08
期刊：
影响因子：
--
通讯作者：
Tatsuya Abe;Tomoharu Ugawa;T. Maeda;Kousuke Matsumoto
中科院分区：
文献类型：
--
作者：
Tatsuya Abe;Tomoharu Ugawa;T. Maeda;Kousuke Matsumoto
软件模型检测存在所谓的状态爆炸问题，而松弛的内存一致性模型更是加剧了这种情况。更糟糕的是，通过内存一致性模型来参数化模型检查，也就是说，为了使模型检查器尽可能灵活，我们可以提供内存一致性模型的定义作为输入，加剧了状态爆炸。本文探讨了多个内存一致性模型的模型检查中状态爆炸的具体原因，提供了一些旨在减轻问题的优化，并将其应用于McSPIN，我们正在开发的内存一致性模型的模型检查器。通过验证并发复制垃圾收集算法的复制协议，验证了优化的效果和McSPIN的实用性。据我们所知，这是第一个模型检查的并发复制协议在宽松的内存一致性模型。
Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.