1. Tatsuya Abe
  2. McSPIN

Overview

HTTPS SSH

McSPIN is a model checker with memory consistency models [1,2,3]. To know an outline of McSPIN, see doc/slide.pdf in this repository [4].

  1. T. Abe and T. Maeda. A general model checking framework for various memory consistency models. In Proc. of IPDPSW'14 (HIPS), pages 332--341.

  2. T. Abe and T. Maeda. Optimization of a general model checking framework for various memory consistency models. In Proc. of PGAS'14, No. 14, 10 pages.

  3. T. Abe and T. Maeda. Towards a unified verification theory for various memory consistency models. In Proc. of LOLA'15, 2 pages.

  4. T. Abe. McSPIN: a model checker with memory consistency models. ALGI'15.

Requirement

Usage

Install the GHC via apt/yum etc.

Install SPIN.

Get McSPIN hg clone https://bitbucket.org/abet/mcspin.

Implement your user-defined memory consistency model app/MyMcm.hs. (cf. Sequential.hs, Tso.hs, Pso.hs, Rmo.hs, etc.)

Compile it $ cd app; ghc -i../src MyMcm.hs.

Write a program test/test.c in tiny C. See test/*.c.

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 0).

However, McSPIN distinguishes the effects from the fetches of the store instructions x=1 and 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 [2] 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[3]=1,3:ref(0)
          McSPIN:1:mem_at_1_on_0[3]=1,3:ref(1)
                McSPIN:0:fetch
                ...
          McSPIN:0:mem_at_0_on_0[2]=1,2:ref(0)
          McSPIN:0:mem_at_1_on_0[2]=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.

Remark

  • McSPIN does not support pointers as SPIN does not.

TODO

  • Write a document for usage.
  • Use stack to make installation easy.