Optimization of a General Model Checking Framework for Various Memory Consistency Models
Tatsuya Abe, Toshiyuki Maeda · 2014
While relaxed memory consistency models contribute optimizations of compilers on multicore CPUs and shared memory distributed programming languages, their relaxedness makes it difficult to write programs correctly. To address this problem, the authors proposed a general model checking framework and implemented a prototype tool McSPIN, which can take a memory consistent model as an input, as well as a program and a property to be checked, in their previous works. However, one big problem of McSPIN was that it was prone to suffer from the state explosion problem, and difficult to be applied to programs other than small example programs. In this paper, we propose optimization approaches for McSPIN to largely reduce the number of state transitions to be explored during model checking so that it can be applied to larger programs. In addition, we actually implemented the optimizations to McSPIN, and this paper gives several experimental results with the optimized McSPIN to show effectiveness of the proposed optimization approaches.