Skip to content
master
Go to file
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 

README.md

mmlib

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

使い方

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

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

mmlibの種類

ファイル名 検査できるメモリモデル
sc.h SC(シーケンシャルコンシステンシ)
tso.h TSO(トータルストアオーダリング)
pso.h PSO(パーシャルストアオーダリング)

インクルード前に定義するマクロ

マクロ名 内容
PROCSIZE プロセスの数を表す整数値 ※1
VARSIZE 共有変数の数を表す整数値
BUFFSIZE ストアバッファサイズを表す整数値 ※2

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

共有変数マクロ

マクロ名 内容
WRITE(s, v) 共有変数sに整数値vを書き込む
READ(s) 共有変数sの値を返す
FENCE() フェンス命令を実行する
INIT(s, v) 共有変数sの初期値をvに設定する ※3
SVAR(p, s) プロセスpが観測する共有変数sの値を返す ※4
GSVAR(s) 共有変数sの値を返す ※4

共有変数は,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 ディレクトリにあります.

About

No description, website, or topics provided.

Resources

Releases

No releases published

Packages

No packages published

Languages

You can’t perform that action at this time.