本リポジトリでは，SPINを使って，メモリモデルに従った実行を検査するためのライブラリ「mmlib」を公開しています．
Promelaモデル中の共有変数へのアクセスにmmlibが提供する共有変数マクロを利用するだけで，弱いメモリモデル上でプログラムを実行しても性質が満たされるかを検査できます．
mmlibはSC，TSO，PSOに対応しています（2017/06/29現在）．

1. mmlibをインクルードする．
2. インクルードした位置より前に，モデルの情報をマクロとして定義する．
3. モデル中の共有変数へのアクセスを，共有変数マクロを使用するように変更する．
4. SPINを使った通常の検査手順で検査する．

標準的なSPINの使用方法については公式HPなどをご覧ください．

※1 initプロセスを除く．
※2 mmlibは書き込みをバッファすることで，弱いメモリモデルに従った実行を再現しています．BUFFSIZEが十分でないと正しく検査できません．

共有変数は，0からVARSIZE-1までの整数値で表されます．
例えば，VARSIZEを2と定義した場合は，0と1を共有変数として使用できます．

※3 initプロセス内で使用するマクロです．
※4 LTL式内で使用するマクロです．

(Promelaで記述したモデルの例)

int x = 0;
int y = 0;

proctype p0() {
  x = 1;
  y = 1;
}

proctype p1() {
  int r0, r1;
  r0 = y;
  r1 = x;
  assert(!(r0 == 1 && r1 == 0));
}

init {
  atomic {
    run p0();
    run p1();
  }
}

(mmlibを使ってTSOのもとでの動作を検査するように書き換えたモデル)

#define PROCSIZE 2
#define VARSIZE 2
#define BUFFSIZE 2
#define x 0
#define y 1
#include "tso.h"

proctype p0() {
  WRITE(x, 1);
  WRITE(y, 1);
}

proctype p1() {
  int r0, r1;
  r0 = READ(y);
  r1 = READ(x);
  assert(!(r0 == 1 && r1 == 0));
}

init {
  atomic {
    run p0();
    run p1();
  }
}

4行目，5行目のようなマクロを定義することで，元のモデルと同じ使い勝手で共有変数を扱うことができます．

もっと多くの例は example ディレクトリにあります．