Name
Title | ||
|---|---|---|
Reordering Control Approaches To State Explosion In Model Checking With Memory Consistency Models |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-72308-2_11 | VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017) |
Keywords | Field | DocType |
Software model checking, Relaxed memory consistency model, State explosion, Instruction reordering control, Concurrent program examination | Software model checking,Programming language,Model checking,Computer science,Theoretical computer science,Consistency model | Conference |
Volume | ISSN | Citations |
10712 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tatsuya Abe | 1 | 18 | 4.00 |
| Tomoharu Ugawa | 2 | 22 | 7.52 |
| Toshiyuki Maeda | 3 | 21 | 3.70 |