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

Tatsuya Abe, Tomoharu Ugawa, and Toshiyuki Maeda. Reordering control approaches to state explosion in model checking with memory consistency models. In Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), volume 10712 of Lecture Notes in Computer Science, pages 170–190. Heidelberg, July 2017. DOI:10.1007/978-3-319-72308-2_11

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.