McSPIN is a model checker with memory consistency models . To
know an outline of McSPIN, see
doc/slide.pdf in this repository .
T. Abe and T. Maeda. A general model checking framework for various memory consistency models. International Journal on Software Tools for Technology Transfer, 19(5):623--647, 2017. DOI:10.1007/s10009-016-0429-y
T. Abe. McSPIN: a model checker with memory consistency models. ALGI'15.
Install the GHC via apt/yum etc.
hg clone https://bitbucket.org/abet/mcspin.
Implement your user-defined memory consistency model
(cf. Sequential.hs, Tso.hs, Pso.hs, Rmo.hs, etc.)
$ cd app; ghc -i../src MyMcm.hs.
Write a program
test/test.c in tiny C. See
Translate the program into a Promela code.
$ cd test; ../app/MyMcm -i1,1 -I../include -O1 test.c.
McSPIN has some command-line options for optimization.
Options with no argument
- -s threads are executed in speculation mode
- -O1 states are restored by truth values of predicates defining a memory consistency model
Option with argument
- -vNUM print (1)generated instructions, (2)an expanded input program, and (3)its intermediate representation (default: 0)
- -iNUM[,NUM[...] set supremes of the number of loop iterations NUM (default: 1)
- -Gstring pass a string to a preprocessor
- -dNUM set depth in iterative deeping mode where 0 means no supreme (default: 0)
- -pNUM set depth in parallel processing mode where 0 means no supreme (default: 0)
Run the generated Promela code by SPIN
$ spin test_MyMcm.pml.
Check the generated Promela code by SPIN
$ spin -a test_MyMcm.pml; gcc -O0 -o pan pan.c ; ./pan -c1. SPIN returns
test_MyMcm.log including results.
Print a counterexample (if the result means that there exists a counterexample) by SPIN
$ spin -t test_MyMcm.pml.
How to See a Counterexample which SPIN tells
A key idea of McSPIN is to distinguish effects from its fetch for any instruction, although model checkers that ignore memory consistency models do not distinguish them.
For example, the program
(x=1; y=1) || (r0=y; r1=x) (often called MP) has usually no counterexample of an assertion
r0 <= r1 (if all the variables are initialized to
However, McSPIN distinguishes the effects from the fetches of the store instructions
y=1. MP has the following counterexample under PSO, which allows reordering between effects of store instructions:
x=1:fetch, y=1:fetch, y=1:effect, r0=y, r1=x, x=1:effect.
To be precise, McSPIN supports three kinds of issue, execute, reflect (see  in detail). The SPIN command
$ spin -t prints the following counterexample:
McSPIN:0:fetch McSPIN:0:[x_at_0_on_0]=1,2:iss McSPIN:0:[x_at_0_on_0]=1,2:exe McSPIN:1:fetch McSPIN:1:[y_at_0_on_0]=1,3:iss McSPIN:1:[y_at_0_on_0]=1,3:exe McSPIN:1:mem_at_0_on_0=1,3:ref(0) McSPIN:1:mem_at_1_on_0=1,3:ref(1) McSPIN:0:fetch ... McSPIN:0:mem_at_0_on_0=1,2:ref(0) McSPIN:0:mem_at_1_on_0=1,2:ref(1) McSPIN:2:fetch McSPIN:2:nop:iss successful termination: exit process1 by timeout successful termination: exit process0 by timeout spin: mp-Pso-1,1-0-0-.pml:663, Error: assertion violated
in which the reflects to the other thread of the store instructions are reordered.
Differences from Papers
- Threads are identified by non-positive integers, that is, zero-based indexing is adopted.
StrictO(an order relation to define memory consistency models) is not a preorder but a strict order.
- McSPIN does not support pointers as SPIN does not.
- Write a document for usage.
- Use stack to make installation easy.