2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

SPIN で弱いメモリ順序のメモリモデルでのプログラムの実行をモデル検査するためのライブラリの改良
松元 稿如1,a)

鵜川 始陽1,b)

安部 達也2,c)

概要：現代の CPU は，プログラムのメモリアクセス命令の実行順序を入れ替える場合がある．しかし，モデル検査器 SPIN はそのような場合を検査しないため十分な検査を行うことができない．そこでこれまでに我々は，SPIN でメモリアクセス命令の順序が入れ替わる場合も検査できるライブラリを開発してきた．我々のライブラリを使えば，トータルストアオーダリング（TSO）とパーシャルストアオーダリング（PSO）に従って命令の順序が入れ替わる場合の検査が可能になる．このライブラリは，複数のスレッドで共有される変数（共有変数）のモデルと，共有変数を読み書きするためのマクロを提供する．しかし，このライブラリには三つの問題がある．第一に，SPIN では安全性や活性のような検査したい性質を LTL（Linear Temporal Logic）式で表現できるが，LTL 式内から我々のライブラリが提供する共有変数を参照できない．第二に，ある条件が成り立つまでスレッドの実行を止めるためによく利用されるガード文からも，共有変数の値を参照できない．最後に，共有変数の初期値は常に 0 になり，ユーザが指定することはできない．そこで本発表では，これらの問題を解決できるようにライブラリを改良した．改良したライブ
ラリを用いていくつかのモデルを作成し，ライブラリの性能を調査した．
キーワード：SPIN，メモリモデル，LTL，モデル検査

An Improvement of a Library for Model Checking
under Weakly Ordered Memory Model with SPIN
Kosuke Matsumoto1,a)Tomoharu Ugawa1,b)

Tatsuya Abe2,c)Abstract: Modern multi-core CPUs may execute memory access instructions of programs out-of-order.
However, the SPIN model checker does not check out-of-order executions, but it only checks in-order executions. We have developed a library for SPIN that enables to check such out-of-order executions with respect
to two memory models, the total store ordering (TSO) and the partial store ordering (PSO). This libraryprovides models of variables shared with multiple threads (shared variables), and read and write macros toaccess them. However, this library has three problems. Firstly, though SPIN accepts LTL (Linear Temporal
Logic) formulas, which are used for representing properties to be checked such as safety and liveness, ourlibrary did not support LTL formulas referring to shared variables. Secondly, guard statements, which areoften used for blocking threads while guard is not executable, could not refer to shared variables. Finally,
the user could not specify initial values of shared variables, but they are initialised with zero. In this presentation, we improved the library to resolve these problems. We made models using our improved library andinvestigated the performance of the library.
Keywords: SPIN, memory model, LTL, model checking1

2

高知工科大学
Kochi University of Technology, Kami, Kochi 782–0003,
Japan
千葉工業大学人工知能・ソフトウェア技術研究センター
Software Technology and Artificial Intelligence ResearchLaboratory, Chiba Institute of Technology, Narashino, Chiba

a)
b)
c)

275–0016, Japanmatsumoto@pl.info.kochi-tech.ac.jp
ugawa.tomoharu@kochi-tech.ac.jp
abet@stair.center1

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

質は LTL 式によって表現できる．SPIN でも，モデルが満

1. はじめにモデル検査器 SPIN はプログラムの検査のために使用されている [6]．Promela という手続き型言語に近い逐次実行
形式の言語によってプログラムの変数の操作や条件分岐などの動作をモデル化し，そのモデルから作成したオートマ
トンが全状態で検査したい性質を満たすかどうかを SPIN
を使って網羅的に検査することでモデル検査を行う．

SPIN はモデル検査の際，プログラムのモデルに記述された順序の通りの実行を検査する．しかし，現代の CPU
はメモリアクセス命令の完了を待たずに，その命令に依存しない後続命令を実行し，先に完了させることがある．マ
ルチスレッドプログラムでこのような実行が起こると，別のスレッドからはプログラムと異なる順序でメモリアクセ
ス命令を実行したように観測されることがあり，モデルに記述された順序通りの実行を検査するだけでは不十分である．どのような条件で先行命令の完了前に後続命令が完了することがあるかは，CPU アーキテクチャ毎に異なり，CPU のメモリコンシステンシモデル（以下，メモリモデ
ル）によって定義されている．マルチスレッドプログラムのモデル検査では，メモリモデルに従ったあらゆる実行を検査する必要がある．しかし，プログラムに加えて，メモ
リモデルに従った実行まで含めたモデルを記述すると，モデルが煩雑になり，モデルに誤りが混入しやすい．
そこで我々はこれまでに，共有変数に対する読み書きが完了する順序に関して，SPIN でメモリモデルに従ったマ
ルチスレッドプログラムの実行を検査できるようにするためのライブラリを開発してきた [15]．本ライブラリは，複数のスレッドからアクセスされる変数（共有変数）のモデ

たすべき性質をモデル中の変数や各プロセスの実行位置（プログラムカウンタ）を用いた LTL 式によって表現できる．例えば，共有変数 want0 が 1 になれば，その時刻以降
いつかはプロセス t0 がラベル CS の位置に到達するという性質が常に成り立つことを表現する LTL は[] (want0 == 1 -> <> t0@CS)と表すことができる．これは 2 章で示すピータソンの相互排除アルゴリズムのモデルで活性の性質を表している．しかし，本ライブラリで共有変数の値を使用するには，一旦READ を使用してローカル変数に読み込まなければならな
いため，上記の LTL 式を記述できない．
二つ目の問題は，ガードからも共有変数を参照できないことである．Promela では，ガードと呼ばれる文を記述することで，ある条件が満たされるまでスレッドの実行を止めることができる．ガードを使うことで，モデルを簡潔に記述でき，モデル検査で探索する状態数も抑えることができる．例えば 2 章で示す 図 2 で使われている(turn == 0 || want1 == 0)というガードは，turn == 0 || want1 == 0 の条件が満たされるまでブロックするという振舞いを簡潔に記述している．しかし，一つ目の問題と同じ原因，つまり，本ライブ
ラリで共有変数の値を使用するには，一旦 READ を使用してローカル変数に読み込まなければならないため，共有変数を参照するガードも記述できない．そのため上記のガードは，下に示すような共有変数をポーリングするループに書き換える必要がある．

do::true -> atomic {ルと，ユーザが記述したモデルから共有変数を読み書きす

READ(turn, x);

るためのマクロを提供する．本ライブラリを使用すること

READ(want1, y);で，メモリモデルに従った動作を考慮せずにモデルを作成

if

するのと同程度の手間で，メモリモデルに従ったあらゆる::(x == 0 || y == 0) -> break;

実行順序を検査できるモデルを作成できる．本ライブラリ::else -> skip;が提供するマクロは，共有変数を対象とする書き込みと読fi;}

み込みの際に使用する．ユーザが共有変数に値を書き込む
際には，WRITE マクロを使用する．WRITE は，第一引数の共有変数に第二引数の値を書き込むマクロであり，例えば共有変数 x に 1 を書き込むには WRITE(x, 1) と書く．ユー
ザが共有変数から値を読み込む際には，READ マクロを使用する．READ は，第一引数の共有変数の値を第二引数のロー
カル変数に格納するマクロであり，例えば，共有変数 x の値をローカル変数 r に読み込むには READ(x, r) と書く．
本ライブラリには三つの問題がある．一つ目の問題は，検査したい性質を線形時相論理（Linear Temporal Logic:

LTL）式で記述する際に，共有変数を参照できないことである．プログラムの安全性や活性などの時間に関連した性

od;
また，ガードが非決定的分岐の条件として用いられる場合，書換えが簡単ではないこともある．
三つ目の問題は，共有変数の初期値を設定できないことである．本ライブラリが共有変数に書き込む唯一の手段として提供している WRITE は，ユーザ定義プロセス内でしか使えない（詳細は 4 章参照）．そのため，ユーザ定義プロ
セスの起動前に共有変数を初期化する手段がない．その結果，共有変数の初期値は Promela の仕様上 0 となってしまう．
そこで本研究では，ライブラリを改良し，これらの問題

22017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日を解決した*1 ． 改良したライブラリはメモリモデルに従っを文として扱う．モデル中のあらゆる文は真か偽かを判定

た実行を検査できる既存のモデル検査器 [3], [12], [13], [14]

され，偽の文は実行されない．偽の文が実行されないことに比べ，モデルの可読性が高い点，LTL で性質を記述でき

で，プロセスの実行が止まることをブロックするという．
例として， 図 1 のピーターソンのアルゴリズムによっる点，軽量である点で優れている．
本論文では，まず予備知識として SPIN（2 章）とメモリて相互排除を行う C のプログラムを，Promela でモデル化

モデル（3 章）
，改良前のライブラリ（4 章）について解説する．まず， 図 1 のプログラムについて説明する．図 1 のする．その後，本章で挙げた問題を解消できるようにライグローバル変数 want0 と want1 は，それぞれスレッド t0

ブラリを改良し（5 章），改良したライブラリを実装し，改と t1 がクリティカルセクションに入ろうとしていること良したライブラリの性能評価を行う（6 章）．さらに，メモを相手のスレッドに知らせるためのフラグである．グロー

リモデルや LTL 式を扱うモデル検査の関連研究について

バル変数 turn は，その時点で優先的にクリティカルセク

言及する（7 章）．最後に，本論文のまとめと今後の展望をションに入ることのできるスレッドを表している．t0 が述べる（8 章）．

クリティカルセクションに入るためにはまず，want0 を 1

2. SPINにすることで，相手のスレッドに自身がクリティカルセク
ションに入ろうとしていることを知らせる．次に，turn をモデル検査器 SPIN は，モデル検査法に基づいてハード操作して相手のスレッドが優先的にクリティカルセクショ

ウェアやソフトウェア，プロトコルなどの自動検証を行う

ンに入れるようにする．その後，want1 が 0 になるか，相ツールである [6]．

手のスレッドの操作によって turn が 0 になるまで待ち状態になる．条件が整えば待ち状態を抜けてクリティカル

2.1 モデル検査法
モデル検査法とは，検査対象の状態が変化する動作に注セクションに入る．クリティカルセクションを抜けると，

want0 を 0 にすることで相手のスレッドに知らせる．

目して記述されたモデルが取り得る状態を網羅的に検査す

図 2 は 図 1 のモデルである．Promela ではスレッドにる形式手法である [5]．例えばプログラムを検査する場合相当するプロセスを記述するために proctype というキー

は，変数の操作や条件分岐などの動作を抽出したモデルをワードを使う．また，ユーザ定義のプロセスよりも先に実作成し，モデルの取り得る全状態，つまり計算機上で実行行される init プロセスが利用できる．ユーザ定義プロセスした時の変数の取り得る値やプログラムの実行位置などがは 21 行目のように run 命令によって実行される*2 ．20 行

期待通りであることを検査する．SPIN を使用してモデル

目から 23 行目の atomic { } で囲まれた範囲は，ひとまと検査するためのモデルは，専用の記述言語 Promela でプ

まりの命令として実行され，実行可能な限りインタリーブ

ログラムと検査したい性質を記述し作成する．作成したモされない．繰り返しは do と od の間に記述するが，図 1 のデルを入力として与えると，SPIN は与えられたモデルを

while による待ち状態は，図 2 の 6 行目の文がブロックすBüchi オートマトンに変換し，そのオートマトンの全状態ることを利用してモデル化している．6 行目のような，続で検査したい性質が成り立つかどうかを網羅的に検査する

く文が実行されるための条件として記述される文をガードことでモデル検査を行う．

という．図 2 では使用していないが，条件分岐は以下のよ

一般にモデル検査法には，有限の状態に収まる検査対象しか扱えないという欠点がある．例えば任意の自然数に対

うに if と fi の間に記述し，「::」の後のガードが真ならば「->」に続く文が実行される．

する実行について検査することはできない．他にも，モデif

ルが大きくなるにつれて検査する状態数が指数的に大きく::(x == 0) -> x = 1;

なるという欠点がある．そのため，モデルを作成する際に::(y == 0) -> y = 1;

は状態数を抑える工夫が重要になる．

fi;
複数のガードが同時に真になった場合は，いずれかのガー

2.2 Promela

ドに続く文が非決定的に実行される．ただし，「::」に続Promela は C に似た構文を持ち，C のマクロを使用でく文が全て偽ならブロックする．Promela では数値型の変きる．マルチスレッドプログラムのモデル記述に向いてお数のほかにチャネル型の変数が用意されており，FIFO 形

り，スレッドに相当するプロセスを記述するためのコンス

式のキューとして扱うことができる．他にも，LTL 式など

トラクトを持つ．プロセス毎に記述された文は記述されたで使用するためのラベルを記述でき，例えば，11 行目の順序通りに他のプロセスの文とインターリーブして実行さ

CS:のように，ラベルを記述することもできる．

れる．Promela では，「;」もしくは「->」で区切られた式*1

本 ラ イ ブ ラ リ と 本 論 文 で 使 用 し た モ デ ル は ，
https://github.com/plasklab/mmlib で公開している．

*2

active proctype というキーワードによって，自動で起動するプロセスも記述できるが，本研究では扱わない．

3

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

1

1

# include < pthread .h >23

int want0 = 0 , want1 = 0 , turn = 0;

2
3

int want0 = 0 , want1 = 0 , turn = 0;

4

proctype t0 () {4

want0 = 1;

void * t0 () {5turn = 1;

6

want0 = 1;

6

7

turn = 1;78while ( true )

8

5

9

9

if ( turn == 0 || want1 == 0)

10( turn == 0 || want1 == 0);
CS : /* Critical Section */want0 = 0;}

10

break ;

11/* Critical Section */11

12

want0 = 0;

12

want1 = 1;

13

return 0;

13

turn = 0;

14

14

}

15

15

16

void * t1 () {16

17

want1 = 1;

17

18

turn = 0;1819while ( true )1920

if ( turn == 1 || want0 == 0)

21

want1 = 0;}
init {

20

22/* Critical Section */22

23

want1 = 0;23

return 0;

24

25( turn == 1 || want0 == 0);
CS : /* Critical Section */atomic {21

break ;

24

proctype t1 () {run t0 ();run t1 ();}}}図 2 Promela で記述された 図 1 のプログラムのモデル
図 1 C で記述されたピーターソンのアルゴリズムによるFig. 2 Promela model for the program in Fig. 1.

相互排除プログラム

Fig. 1 Mutual exclusion programusing Peterson’s algorithm in C.

2.3 モデルの満たすべき性質の記述方法
SPIN でモデルが満たすべき性質を記述する方法には，
assert 文で記述する方法と LTL 式を使う方法がある．
assert 文を使用する方法は，assert( ψ ) という文をモデル中の任意の位置に挿入することである．ただし，ψ
は以下で定義される論理式である．

連した性質を表現するための論理式である．LTL 式 φ は以下で定義される論理式である．

φ ::= ⊤ | P | ¬ φ | φ ∨ φ | X φ | φ U φ
X φ は「次の時点で φ が成り立つ」ことを意味している．
φ0 U φ1 は「φ1 が成り立つようになるまでは φ0 が成り立
ち続け，かつ，いつか φ1 が成り立つ」ことを意味している．便利のため，以下の略記を使用する．

3φ ≡ ⊤ U φ

ψ ::= ⊤ | P | ¬ ψ | ψ ∨ ψ
ここで ⊤ は真であることを意味する命題定数である．P

2φ ≡ ¬3¬φ

は SPIN で利用可能な原子命題を表す命題変数であり，例

3 φ は「いつか φ が成り立つ」ことを意味し，2 φ は「ずっえば， 変数や即値の等号（==）や比較演算子（<）を用いと φ が成り立ち続ける」ことを意味している．

て表現される命題である．詳しくは文献 [6] を参照された

LTL 式が意味するものの定義を以下で与える．SPIN がい．¬ ψ は ψ の否定を表し，ψ0 ∨ ψ1 は ψ0 と ψ1 の論理探索するモデルの実行経路の集合は一つの状態遷移系と考え和を表している．論理積や含意は略記として定義する．モられる．この状態遷移系をクリプキモデル M = ⟨M, R, val ⟩デルに挿入された位置でその assert 文中の式が真ならばで書くことにする．ただし，M は状態の集合，R は M 上

なにもせず，偽ならばエラーを出力し検査を打ち切る*3 ．

の関係，val は命題変数から M の部分集合への関数であassert 文が挿入された位置においての真偽のみを扱う

る．M 上の経路 π を，R で関係づけられている M の元のに対し，LTL 式は，ある性質が与えられた時「その性質の（有限とは限らない）列とし，π の i 番目（先頭は 0 番

がいつか真になる」といった，（ある時点以降の）時間に関目とする）の状態を π(i) ，π から i 番目の状態以降の列を*3

打ち切らないこともできるが，本論文では打ち切る場合のみを扱う．

π i と書くことにする．M 上の経路 π による LTL 式 φ の
解釈 M, π ⊨ φ を

4

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

初期値 x = 0; y = 0;

M, π ⊨ ⊤ ⇐⇒ 真である
M, π ⊨ P ⇐⇒ π(0) ∈ val (P )M, π ⊨ ¬ φ ⇐⇒ M, π ̸⊨ φ
M, π ⊨ φ0 ∨ φ1 ⇐⇒ M, π ⊨ φ0 または M, π ⊨ φ1
M, π ⊨ X φ ⇐⇒ M, π 1 ⊨ φスレッド A

スレッド BStore(x, 1);

Store(y, 1);

Load(y, eax);

Load(x, ebx);

図 3 SC と TSO で実行結果が異なる場合のあるプログラム例

Fig. 3 Example of program thatM, π ⊨ φ0 U φ1 ⇐⇒ ある j ∈ N が存在して M, π j ⊨ φ1 ，かつ，任意の i < j に対して M, π i ⊨ φ0

can yield diﬀerent results in SC and TSO.

デルを，異なるメモリアドレスに対する上記の四つの実行
順序について，それぞれ CPU が後続命令を先行命令の完と定義する．この定義より，了を待たずに実行し完了させることがあるかを定義したもM, π ⊨ 3 φ ⇐⇒ ある i ∈ N が存在して M, π i ⊨ φのとする．以降，あるスレッドが実行したメモリアクセス

M, π ⊨ 2 φ ⇐⇒ 任意の i ∈ N について M, π ⊨ φ

命令の列が，他の全てのスレッドからは異なる順序で実行i

されたかのように観測される場合があることを，実行順序である．M 上の m0 ∈ M を始点とする任意の経路 πによる LTL 式 φ の解釈 M, π ⊨ φ が満たされるとき，M, m0 ⊨ φ と書く．

が緩和されているという．
メモリアクセス命令の実行順序が緩和されているメモリ
モデルを採用しているアーキテクチャは，プログラムの動Promela では，含意は ->，3 は <>，2 は [] と書かれ作がユーザの想定とは異なる場合がある．そのようなアーる．図 2 において，want0 == 1 が成り立てば，いつかはキテクチャでは，メモリアクセス命令の実行順序を強制す

t0@CS の位置に実行が移ることが常に成り立つという活性る命令としてフェンス命令を提供している．フェンス命令の性質は，を挿入することで，フェンス命令に先行するメモリアクセ[](want0 == 1 -> <> t0@CS)と記述する．

ス命令は，必ずフェンス命令の後続のメモリアクセス命令
より前に完了する．

LTL 式で表された性質を SPIN で検査する場合，性質の本研究では，いかなる実行順序も緩和されないシーケン

否定を表す LTL を never プロセスという特殊なプロセスに

シャルコンシステンシ（SC）[8]，ストア → ロードの実行順変換する*4 ．never プロセスは他のプロセスとは独立に動序が緩和されているトータルストアオーダリング（TSO）

作し，never プロセスが性質の否定を表す LTL を満たすと，[4]，ストア → ロードとストア → ストアの実行順序が緩和

never プロセスが表す Büchi オートマトンが受理状態を含されているパーシャルストアオーダリング（PSO）[4] の三むループに入り，エラーが出力され検査が打ち切られる．

つのメモリモデルを扱う．図 3 に，SC と TSO で実行結

3. メモリモデル

果が異なることがあるプログラムの例を示す．Store(x,1) はメモリアドレス x に 1 を書き込むことを，Load(y,現代の CPU は最適化の際に，先行命令に依存しない後eax) はメモリアドレス y の値を eax レジスタに読み込む

続命令を実行し，先に完了させることがある．その結果，ことを示す．例えば，スレッド A の 2 行目で y から 0 を読

マルチスレッドプログラムにおいて，それぞれのスレッド

み込んだ場合を考えると，SC ではスレッド B の 2 行目では，自身以外のスレッドが実行したメモリアクセス命令のx から 1 を必ず読み込むが，TSO ではストア → ロードの列が，プログラムの順序とは異なる順序で実行されたかの実行順序が緩和されているため 0 を読み込むことがある．

ように観測する場合がある．どのような条件で先行するメ
モリアクセス命令の完了前に後続のメモリアクセス命令を

4. 既存のライブラリ完了させることがあるかは，CPU アーキテクチャ毎に異

本章では，改良前の本ライブラリについて解説する．

なり，CPU のメモリモデルによって定義されている．

本ライブラリは，共有変数のモデルと，ユーザが作成し本研究では，メモリアクセス命令として書き込み命令

たモデルからそれらに対してメモリモデルに従った読み書（ストア）と読み込み命令（ロード）を考え，あるスレッド

きを行うためのマクロを提供している．各スレッドは，共がメモリアクセス命令 A の後にメモリアクセス命令 B を

有変数を介してのみメモリモデルの影響を受け，CPU がメ実行したという順序を A → B と表すことにする．すると，モリアクセス命令の列の順序を入れ替えて完了させた結果

二つのメモリアクセス命令の実行順序として，ストア →を観測する．よって，メモリモデルに従ったモデル化を行

ストア，ストア → ロード，ロード → ストア，ロード →うのは，共有変数と，それらに対する読み書きのみで十分

ロードの四つを考えることができる．本研究ではメモリモである．メモリモデルの影響を受けないローカル変数に対*4LTL 式を Promela モデル中に記述する方法もある．

する読み書きは通常の Promela と同様に行う．以降，ユー

5

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

ザが作成したモデルをユーザモデルといい，ユーザモデル

本ライブラリでは，共有変数を 0 から VARSIZE − 1 までの中の init 以外のユーザ定義プロセスをユーザプロセスとメモリアドレスでモデル化しており，これらのマクロの引いう．

数では共有変数の代わりにメモリアドレスを指定する．

本ライブラリが扱う SC，TSO，PSO の三つのメモリモ

WRITE(a, v)

デルで緩和されるメモリアクセス命令の実行順序は，スト

メモリモデルに従った動作をするストアを提供する．

ア → ロードとストア → ストアのみである．どちらの実行

a はストア対象のメモリアドレス，v は書き込む値で順序も，後続のメモリアクセス命令が先行するストアよりある．

前に実行が完了する場合があることを表している．そのた

READ(a, x)

め，これらのメモリモデルに従った動作をするメモリアク

メモリモデルに従った動作をするロードを提供する．

セス命令をモデル化するためには，ストアの結果が後続の

a はロード対象のメモリアドレス，x は読み込んだ値

メモリアクセス命令よりも後にメモリに反映される場合がを格納したいローカル変数である．

あるようにすればよい．本ライブラリでは，ユーザプロセ
スが実行したストアの内容を格納し溜めておくためのスト

FENCE()
フェンス命令を提供する．

アバッファと，ストアバッファの中身をメモリに反映する

これら三つ以外に，実際の CPU では CAS（Compare and特別なプロセスであるメモリプロセスを導入するアイデア

Swap）命令等のアトミックなメモリアクセス命令も提供さによって，TSO と PSO に従った動作を実現している． な

れているが，本ライブラリではそれらに対応するマクロを

お，プログラムの実行順序とは異なる順序で実行されたか提供しない．それでも，本ライブラリが提供する命令を組のように観測されるのは，自身以外のスレッドが実行したみ合わせることで，いくつかのアトミック命令はユーザがメモリアクセス命令だけである．つまり，自身が実行した作成することができる．例えば SPARC TSO の CAS 命

ストアは即座にロードできる．これを実現するために，各令は Promela の atomic ブロックと READ，WRITE，FENCE

ユーザプロセスに自身が実行したストアの内容を記録して命令を組み合わせることで作ることができる．

おく仕組みとして共有メモリのコピーを導入している．この仕組みを使って，自身が実行したストアで書き込まれた変数からの読み込みは，そのストアが共有メモリに反映されるまでは共有メモリを介さず，共有メモリのコピーからロードするようになっている．
この設計では，ユーザプロセスで atomic ブロックを実
行中はストアバッファが一杯になってユーザプロセスがブ

以下では，本ライブラリが提供するメモリアクセス命令の実装を述べる．
どのメモリモデルでも共有変数の集合を配列として表している．

SC では，WRITE と READ は，それぞれ通常の Promela と同様に共有変数に対して書き込みと読み込みを行い，FENCE
は何も動作をしない．

ロックする場合を除いて，メモリプロセスの実行が進まな

TSO では，ストア → ロードの実行順序が緩和されていい．そのため共有メモリへの反映が行われないことになる．

るため，WRITE が後続の READ よりも後にメモリに反映さ

しかし，atomic ブロックを実行しているプロセスは自身のれることがある．そのために，メモリプロセスと FIFO 形

ストアを共有メモリを介さずにロードできることと，それ式のストアバッファ，共有変数のコピー，各共有変数に対以外のユーザプロセスは実行できないことから，atomic ブするストアが幾つストアバッファに格納されているかを

ロック実行中にストアバッファの中身がメモリに反映され数えるためのカウンタを導入する．ストアバッファと共有たとしても atomic ブロック実行中直後に反映されるのと変数のコピー，カウンタはユーザプロセス毎に用意してお同じ結果になる．

り，それぞれプロセスのプロセス ID をインデックスとす本ライブラリが提供するマクロを使用するには，ユーザる配列になっている．メモリプロセスは，以下の手順をア

モデルが持つプロセスの数や共有変数の数などをパラメタ

トミックに実行し，各ユーザプロセスの書き込みを共有変として与える必要がある．具体的には，ユーザモデルが持数に反映する．

つプロセスの数（PROCSIZE），共有変数の数（VARSIZE），(1) いずれかのユーザプロセスが持つストアバッファを選

ストアバッファのサイズ（BUFFSIZE）の三つを，ユーザ択し，中身を先頭から一つだけ非決定的に取り出す．

モデルで本ライブラリをインクルードする前にマクロとし(2) (1) で取り出したストアの結果を共有変数に反映する．

て定義する．ただし，BUFFSIZE は同時に緩和できるスト(3) (1) で選択したストアバッファを持つユーザプロセス

アの数の制限になっているため，BUFFSIZE が十分な大きのカウンタの，ストアを反映した共有変数に対応する

さでない場合は，検査漏れが生じる危険がある．本ライブ

値を減らす．

ラリでは，これらのパラメタの設定はユーザの責任として

WRITE は図 4 に示すコードのように，実行したユーザプ

いる．

ロセスのプロセス ID に応じて，ストアバッファ（queue）

本ライブラリが提供しているマクロは以下の通りである．

に引数のメモリアドレスと書き込みたい値の組を，引数

6

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

1

# define (s , v ) {\1

# define (s , v ){\2

atomic {\2

atomic {\3

queue [ _pid ]! s , v ;\3

( len ( queue [( _pid )* VARSIZE +( s )]) < BUFFSIZE );\4buffer [ _pid * VARSIZE + ( s )] = v ;\4

queue [( _pid ) * VARSIZE + ( s )]! v ;\5

counter [ _pid * VARSIZE + ( s )]++;\

5buffer [( _pid ) * VARSIZE + ( s )] = v ;\

6

}\

6

7

}

7

}\

8

}

gcounter ++;\

図 4 TSO の WRITE マクロの実装
図 6

Fig. 4 Implementation of WRITE macro for TSO.

PSO の WRITE マクロの実装

Fig. 6 Implementation of WRITE macro for PSO.
1

# define (s , v ){\2

atomic {\1# define (s , v ){\

3

if \

2

atomic {\

3

if \

4

::( counter [ _pid * VARSIZE + ( s )] == 0)\5-> v = shared_memory [ s ];\6-> v = buffer [ _pid * VARSIZE + ( s )];\

8::( len ( queue [( _pid )* VARSIZE +( s )]) == 0)\5:: else \74-> v = shared_memory [ s ];\6:: else -> v = buffer [( _pid )* VARSIZE +( s )];\

7

fi ;\

fi ;\

9

}\

8

}\

10

}

9

}

図 5 TSO の READ マクロの実装

図 7

PSO の READ マクロの実装

Fig. 5 Implementation of READ macro for TSO.

Fig. 7 Implementation of READ macro for PSO.

のメモリアドレスに対応する共有変数のコピー（buffer）の値を読み込むように実装しているが，PSO ではチャネル

へ書き込みたい値を書き込み，カウンタ（counter）の値の長さを取得できる len 関数を利用して実装している．そを一つ増やす，という手順をアトミックに実行する．ここのため，PSO では図 7 に示すようにカウンタは必要ない．

で pid は WRITE を実行したプロセスの ID，s はメモリア

FENCE は TSO と同様である．ストアバッファが共有変数

ドレス，v は書き込む値である．READ は図 5 に示すコー毎に分かれているため，先行するストアと後続のストアのドのように，実行したユーザプロセスが持つストアバッ

書き込み対象の共有変数が異なる場合は，インタリーブの

ファの中身に応じて，引数のメモリアドレスに対応する共仕方によっては先行するストアが後続のストアが共有変数

有変数（shared memory）もしくは共有変数のコピーの値に反映された後で共有変数に反映される場合があり，ストを引数のローカル変数に格納する，という手順をアトミッ

ア → ストアの実行順序を緩和できる．ストア → ロードのクに実行する．メモリプロセスは，ユーザプロセスとイン

実行順序については TSO と同様に緩和できる．

タリーブしながらストアバッファの中身を共有変数に反映するため，インタリーブの仕方によって先行するストアが以下では，本ライブラリが提供するマクロを使用する方法を述べる．

後続のロードが実行された後で共有変数に反映され，スト

図 8 は， 図 2 のモデルのうち，グローバル変数とプロセ

ア → ロードの実行順序を緩和できる．FENCE は，各プロ

ス t0 を本ライブラリを使用するように変更したモデルでセスが持つストアバッファの中身を直ちに全て共有変数にある．1 行目から 3 行目まででパラメタのマクロを定義し反映する．

ている．プロセスは t0 と t1 の二つであるため，PROCSIZEPSO では，ストア → ストアの実行順序が緩和されていは 2 と定義している．共有変数は want0 と want1，turn

るため，WRITE が後続のメモリアクセス命令よりも後にメの三つであるため，VARSIZE は 3 と定義している．共有変

モリに反映されることがある．そのために，ユーザプロセ

数への書き込みの数はどのプロセスでも高々三回であるた

ス毎かつ共有変数毎にストアバッファが用意されている．

め，BUFFSIZE は 3 と定義している，続く 4 行目から 6 行

WRITE は図 6 に示すように実行したユーザプロセスのプ

目は，モデルの可読性を向上させるためのマクロである．

ロセス ID に対応するストアバッファのうち，書き込み対

共有変数は 0 から VARSIZE − 1 までの整数で表すため，4象の共有変数に対応するストアバッファに書き込みたい値

行目から 6 行目のようにマクロを定義することで元のユーのみを格納する．ここで，gcounter はストアバッファにザモデルと同じ使い勝手で共有変数を扱える．7 行目でイ

格納されているストアの総数を管理するカウンタである．

ンクルードしている tso.h は，本ライブラリのうち，TSO

READ は，TSO ではカウンタの値を確認しながら共有変数に従った実行を検査するためのライブラリである．8 行目

72017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

1

# define PROCSIZE 2

旦ローカル変数に格納し，そのローカル変数を組み込んだ2# define VARSIZE 3

式を評価することになる．しかし，各プロセスがインター3# define BUFFSIZE 3

リーブしながら実行されるため，式を評価する直前に共有

4# define want0 0

変数の値を読み込んだとしても，式を評価した時に最新の

5# define want1 1

値であるとは限らない．そのため，本ライブラリを使用す6# define turn 2

7# include " tso . h "ると，ユーザモデル中の共有変数を参照するガードをそのまま用いることはできず，図 8 の 14 行目から 24 行目の89

ような書換えが必要になる．そこで本研究では，これまで

proctype t0 () {10

int eax ;の共有変数の値を一旦ローカル変数に格納する READ の代

11

int ebx ;わりに，共有変数の値を直接返す新しい READ を提供する．

12

WRITE ( want0 , 1);

これによりガードから共有変数を参照できるようになる．

13

WRITE ( turn , 1);

14

do

15

本研究では，以下のような新しい READ マクロを提供する．

:: true -> atomic {16

READ ( turn , eax );17

READ ( want1 , ebx );

18

if

19

::( eax == 0 || ebx == 0)-> break ;21:: else -> skip ;
fi ;

23

}

24
25
27

有変数 s の値を返す．
変数に値を書き込むには WRITE を使用する必要がある．共有変数の初期値はユーザプロセスを実行する前に設定する必要があるが，WRITE はユーザプロセスでしか使用できな
い．そのため，共有変数の初期値を設定できず，共有変数の初期値は Promela の仕様により 0 となる．そこで本研究

od ;CS : /* Critical Section */26

メモリモデルに従った動作をするロードを提供し，共共有変数は本ライブラリが管理しており，ユーザが共有

20
22

READ(s)WRITE ( want0 , 0);}では，init プロセス中で共有変数を初期化できるように，
以下のような初期値を設定するためのマクロを提供する．

INIT(s, v)
図 8 改良前のライブラリを使用したピータソンの相互排除アルゴリズムのモデルの一部

Fig. 8 Part of Promela model with the library of the previous
version for mutual exclusion program using Peterson’salgorithm.

共有変数 s の初期値を v に設定する．
このマクロは，ストアバッファを介さずに共有変数の配列に直接書き込む．

LTL 式を使って検査を行う際にも，READ では直接共有
変数の値を参照できないため，共有変数を参照した LTL 式は記述できない．さらに，READ は実行するユーザプロセ

以降は，共有変数を対象とする書き込みと読み込みを本ラスのプロセス ID に依存するため，新しい READ を使用しイブラリが提供するマクロを使用するように変更したモデても共有変数を参照する LTL 式は記述できない．そこでルである．ただし， 図 2 の 8 行目から 10 行目は，本ライ

本研究では，専用のマクロを提供することで，LTL 式から

ブラリでは共有変数を参照するガードを通常の Promela と共有変数を参照できるようにする．ただし，メモリモデル

同じように記述できないために図 8 の 14 行目から 24 行目

によってはプロセス毎に観測できるメモリの値が異なる場のように繰り返しを含むモデルに書き換えた．

合がある．そのため本研究では，以下のように，共有メモ

5. ライブラリの改良
本ライブラリには二つの制約がある．一つ目は，共有変数の値を読み出すには READ を使用して，一旦ローカル変数に格納しなければならないことである．そのため，例えば式の中で直接共有変数の値を参照できない．二つ目は，WRITE と READ は実行したプロセスのプロセス ID に依存した実装のため，ユーザプロセスでしか使用できないこと

リに反映された共有変数の値を参照する GSVAR マクロに加え，ある特定のプロセスから観測できる共有変数の値を参照する SVAR マクロを提供する．

GSVAR(s)共有変数 s の値を返す．

SVAR(p, s)
ユーザプロセス p から観測できる共有変数 s の値を返す．

である．例えば init プロセスや LTL 式では使用できない．

なお，共有変数への書き込みを一切行わないプロセスを本章では，これらの制約による問題を解決できる新しいマ

用意すれば，そのプロセスが実行した SVAR の結果は常にクロを提供するように，本ライブラリを拡張する．

GSVAR と同じになる．そのため，SVAR のみを使用して実際ユーザが共有変数の値を参照する式を記述するには，一の共有変数の値を参照できる．しかし，そのために用意す82017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

1
2

# define READ ( s )\( counter [ _pid * VARSIZE + ( s )] == 0 - >\1

# define (s , v ){\2

atomic {\3

shared_memory [ s ] :\3

int tmp = v ;\4

buffer [ _pid * VARSIZE + ( s )])4queue [ _pid ]! s , tmp ;\5

buffer [ _pid * VARSIZE + ( s )] = tmp ;\図 9 TSO の新しい READ マクロの実装

6

counter [ _pid * VARSIZE + ( s )]++;\

Fig. 9 Implementation of new READ macro for TSO.

7

tmp = 0;\ /* 不要な状態を作らないため */

8

}\

9

}

るプロセスはユーザモデルと関係ない無駄なプロセスであ
図 10 TSO の新しい WRITE マクロの実装るため，本研究ではそれぞれの共有変数の値を参照する仕Fig. 10 Implementation of new WRITE macro for TSO.

組みを GSVAR マクロとして提供する．
以下では，新しく提供するマクロの実装と使用方法を述
べる．

1
2

5.1 ガードから共有変数を参照するためのマクロ
本節では，ガードから共有変数を参照するための，共有変# define (p , s )\( counter [ p : _pid * VARSIZE + ( s )] == 0 - >\3

shared_memory [ s ] :\4

buffer [ p : _pid * VARSIZE + ( s )])\

数の値を直接返す新しい READ の実装と使用方法を述べる．

図 11 TSO の SVAR マクロの実装

SC では特別な工夫は必要なく，引数の共有変数の値をFig. 11 Implementation of SVAR macro for TSO.

通常の Promela の方法で返すように実装する．TSO では，
図 9 のように，実行したプロセスのプロセス ID に対応するストアバッファに引数の共有変数を対象とするストアが

5.2 LTL 式から共有変数を参照するためのマクロ
本節では，LTL 式から共有変数の値を参照するための格納されていなければ共有変数の値を，格納されていれば

GSVAR と SVAR の実装と使用方法を述べる．

プロセスのプロセス ID に対応する共有変数のコピーの値

5.2.1 実装を返すように実装する．PSO では，実行したプロセスのプ

SC では特別な工夫は必要なく，通常の Promela の方法

ロセス ID に対応するストアバッファのうち，引数の共有

で共有変数の値を返すように実装する．具体的には，GSVAR

変数に対応するストアバッファが空なら共有変数の値を，

は引数の共有変数の値を返すように実装し，SVAR は第一

空でないなら実行したプロセスのプロセス ID に対応する

引数のプロセスによらず第二引数の共有変数の値を返すよ

共有変数のコピーの値を返すように実装する．

うに実装する．

これまでの READ は，共有変数 x の値をローカル変数 a

TSO では，各プロセスが書き込んだ内容がプロセス毎に読み出す際は，のストアバッファに溜まっていることに注意する．GSVAR

READ(x, a);は，ストアバッファの内容に関係なく引数の共有変数の値のように使用したが，新しく提供する READ は，

a = READ(x);を返すようにする．SVAR は，図 11 のように，第一引数のプロセスのプロセス ID に対応するストアバッファに第二のように使用する．新しい READ を使用することで，図 8引数の共有変数を対象とするストアが格納されていなけれの 14 行目から 24 行目の繰り返しを含む待ち状態を，以下ば共有変数の値を，格納されていればそのプロセスのプロのように繰り返しを含まないよう 1 文でモデル化できる．

セス ID に対応する共有変数のコピーの値を返すようにす(READ(turn) == 0 || READ(want1) == 0);

る．なお，Promela で特定のプロセスのプロセス ID はプ

ただし，新しい READ は直接共有変数の値を返すために，

ロセス名: pid のように参照できる．

WRITE の第二引数の中で使われる可能性がある．READ は
ストアバッファに要素が格納されているかどうかで動作がPSO も TSO と同様の方法で定義する．
5.2.2 使用方法変わるため，WRITE の第二引数に WRITE の書き込み先であLTL 式中で共有変数の値を参照する際，参照したい値はる変数を読みだす READ が使われると問題が起こる．図 4

共有変数が持つ値なのか，いずれかのプロセスから観測さに示した TSO の WRITE の実装では，ストアバッファに格れる共有変数の値なのかに注意する必要がある．TSO や納する時と共有変数のコピーに格納する時で READ で読み

PSO では，これらは異なることがあるからである．例えば込む箇所が異なるからである．そこで，本研究では TSO

図 2 のモデルで，共有変数 want0 が 1 になっていてもいつで図 10 のように第二引数を一旦ローカル変数に格納するかは 0 に戻って，14 行目にあるプロセス t1 のように WRITE の実装を変更した．PSO についても同様に変更した．

(turn == 1 || want0 == 0);のブロックが解除されることを検査したいとする．その時

92017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

は，プロセス t1 からどう観測されるのかが重要なので，つので，π 1 は M 上の m0 を始点とする経路である．ゆえ

SVAR を使って，に，M, π 1 ⊨ φ である．
定義より，[](SVAR(t1, want0) == 1 -><>SVAR(t1, want0) == 0)とするのがよい．また，図 2 のモデルには現れていないプ

M′ , π ⊨ 2 (flag → φ)

ロセスがあり，そのプロセスから共有変数 want0 の値の変⇐⇒ 任意の i ∈ N について M′ , π i ⊨ flag → φ

化がどのように観測されるかに興味がある時は，次の例の⇐⇒ M′ , π 1 ⊨ flag → φ かつ

ように GSVAR を使って共有変数の値を直接調べることができる．

任意の i ̸= 1 について M′ , π i ⊨ flag → φ⇐⇒ M′ , π 1 ⊨ φ[](GSVAR(want0) == 1 -><>GSVAR(want0) == 0)
ところで，Promela では，初期値を明示しない場合は変数の初期値は 0 になる．本研究では，共有変数の初期値を設定するために INIT を提供するが，INIT で初期値を設定するまでは共有変数の値は 0 のままである．そのため，例
えば<> (GSVAR(x) == 0) などの LTL 式は初期状態で成り立ってしまい，正しく検査できない．しかし，初期化が完了したことを明示的に示すように，ユーザがユーザモ
デルと LTL 式を変更すればこのような性質も検査できる．

であり，補題 1 より，M′ , π 1 ⊨ φ であることと M, π 1 ⊨ φであることは同値なので，M′ , m0′ ⊨ 2 (flag → φ) である．

M, m0 ̸⊨ φ と仮 定す る．定 義 より ，M 上の m0 を始 点 と す る 経 路 π が 存 在 し て M, π ̸⊨ φ で あ る ．補
題 1 より，M′ , π ̸⊨ φ である．m0 ∈ val ′ (flag) なので，

M′ , π ̸⊨ flag → φ である．π にプレフィックス m′0 を追加した列（m′0 π と書く）は M′ 上の経路なので，M′ , m′0 π ̸⊨

2 (flag → φ) であり，ゆえに，M′ , m′0 ̸⊨ 2 (flag → φ) である．

例えば，モデルの初期化が完了したことを示すフラグを通常のグローバル変数として導入し，init プロセス内の共有

LTL 式内で共有変数以外のグローバル変数やローカル

変数の初期化が終わった位置でフラグを操作する方法があ

変数，ラベルなどのライブラリが管理しないものについて

る．フラグとしてグローバル変数 flag を導入し，以下のは，2.3 節で述べたような通常の Promela と同じ方法で参ように操作する．

照する．

flag = 1; flag = 0;
この初期化が終わって flag がセットされている状態を m0と書くことにする．このような状態は一状態しかない．さらに，LTL 式 φ を以下のように変形する．

5.3 モデル化の正しさ
本ライブラリでは，ストアバッファと共有変数のコピーを用いて TSO と PSO をモデル化した．これはメモリモ
デルの操作的なモデル化では一般的であり，既存研究で2 (flag → φ)も同様のモデル化で説明されている [10], [13]．本節では，

以 下 で は ，元 々 の LTL 式 φ と 変 換 後 の LTL 式

2 (flag → φ) が同じ性質を表現することを証明する．
クリプキモデル M を M = ⟨M, R, val ⟩， m0 ∈ M ，
′

′

′

′

val (flag) = ∅ と仮定する．M = ⟨M , R , val ⟩ を

Travkin らの TSO と PSO のメモリモデルの説明 [13] との対応を示すことで，本研究で改良したライブラリで用いたモデル化の正しさを説明する．

Travkin らは TSO と PSO のメモリモデルを，各プロセスがストアバッファを持つモデルとして説明している．

m′0 ̸∈ MR′= R ∪ {⟨m′0 , m0 ⟩}M ′ = M ∪ {m′0 }′Travkin らのストアバッファは，共有メモリや他のプロセ

val (flag) = {m0 }スのストアバッファと一貫性がないキャッシュとしても働′く．プロセスからの書き込み（write 操作）はストアバッ

任意の p ̸= flag について val (p) \ {m′0 } = val (p)ファでキャッシュされ，ストアバッファを時々フラッシュを満たすクリプキモデルとする．

する（flush 操作）ことで共有メモリに反映される．なお，

補題 1. φ が flag を含まないとき，M, π ⊨ φ であること

flush 操作はストアバッファの最も古い書き込み一つだけをと M′ , π ⊨ φ であることは同値である．

共有メモリに反映する操作になっている．プロセスからの証明. φ に関する帰納法による．

読み込み（read 操作）では，対象の変数の値がストアバッ

命題 2. φ が flag を含まないとき，M, m0 ⊨ φ であることと M′ , m′0 ⊨ 2 (flag → φ) であることは同値である．
′

ファにキャッシュされていない時だけ共有メモリから読み込む．フェンス（fence 操作）は flush 操作を強制してスト
アバッファを空にする操作として説明されている．

上の m′0 を始点

本ライブラリでは，Travkin らのストアバッファの，共とする経路とする．π は m′0 m0 というプレフィクスを持

有メモリへの書き込の反映を遅延させる機能とキャッシュ

証明. M, m0 ⊨ φ と仮定する．π を M

102017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日の機能を別の仕組みで実現している．前者は本論文ではと同じ方法で調査した．具体的には x86-TSO に従ったメモ

Promela のチャネル（本論文ではこれをストアバッファとリモデルになっているかどうかをテストするためのテスト呼んでいる）とメモリプロセスによって実現している．後プログラム集 (x86-TSO リトマステスト) [11] を用い調査し者は共有変数のコピーにより実現している．本ライブラ

た．x86-TSO リトマステストにはプログラムと x86-TSO

リではメモリプロセスが書き込みを反映させるのに対しのもとで起こり得る結果や起こり得ない結果が記されていて，Travkin らの説明ではユーザプロセスが自ら非決定的る．本ライブラリの TSO のモデルは x86-TSO リトマステに flush 操作を行うという違いがある．しかし，一つの書

ストの期待される結果に合致するかを，PSO のモデルは既き込みを共有メモリに反映させる操作は不可分に行われる存のメモリモデルを考慮したモデル検査器である McSPIN

ため，どのプロセスが行ってもモデル検査の結果に影響せ[3] での実行結果と比較することで調査した．その結果，全ず，両者に本質的な違いはない．

てのテストにおいて期待する結果になった．

Travkin らの write 操作と fence 操作は本ライブラリの
WRITE マクロ と FENCE マクロに対応している．read 操作

以下では LTL 式を仕様した検査が正しくできるかどうかの調査と性能評価の結果を示す．

は改良前の本ライブラリの READ マクロと同じように，ローカル変数を引数にとって共有変数の値をレジスタにコピー

6.1 実験方法する意味論になっている．したがって，改良後の READ マ

共有変数を参照する LTL 式を使用した検査が正しくでき

クロと厳密には対応しないが，改良後の READ マクロ をるかどうかの調査と性能の評価には，文献 [16] と文献 [9] で使って紹介されているモデルのうちの一部を使用した．文献 [16]a = READ(x);からは， 表 1 に示す，LTL 式を使用しかつ検査結果が述べのようにローカル変数（a）に共有変数（x）の値を読み込られているモデルを使用した．ただし，本ライブラリは数

むことはできる．このような使い方をすることで，本ライ値型の共有変数のみを扱うため，本ライブラリでは扱わなブラリは Travkin らの TSO と PSO の説明に沿った振舞い

いチャネル型の共有変数を持つ一つのモデルは除外した．

をする．

「モデル名」の項目はモデルの文献 [16] 中で記載されていそれ以外の使い方で READ マクロを使う場合も Travkin

る箇所を表す．表 1 のモデルのうち，練習 2.1 と問題 3.7

らの TSO や PSO の説明の範囲を超えた振舞いはしない．

は活性と安全性を LTL 式で検査する方法が記載されてい例えば，たため，それぞれを検査した．文献 [9] からは， 表 2 に示

WRITE(x, READ(y))

す，2 プロセスについての相互排除アルゴリズムのモデルのように WRITE マクロの引数として READ マクロを使った

例を使用した．
「モデル名」の項目はモデルで使用されてい場合は，5.1 章で示したように，WRITE マクロの中で READ

る相互排除アルゴリズム名を表す．文献 [9] では，それぞマクロ の結果を一時的なローカル変数に格納してそれを書れのモデルの TSO と PSO に従った実行を検査する際に，き込む操作になるので，相互排除を成り立たせるためにフェンス命令を挿入するべ

atomic{tmp = READ(y); WRITE(x, tmp)}

き位置が明示されている．つまり， 表 2 に示すモデルは，と同じ振舞いになり Travkin らの TSO や PSO の範囲を超安全性が成り立つモデルである． これらのモデルには，共えない．また，有変数の読み込みや，共有変数を参照するガード，共有変(READ(x) == 0)のようにガードとして使う場合は，

atomic{tmp = READ(x); (tmp == 0)}数の初期値を設定するモデルが含まれている．

LTL 式内から共有変数を参照するマクロが正しい動作をするかどうかは，文献 [16] で述べられている検査結果に置換えたモデルの実行トレースのうち，READ(x) の結果との比較と，文献 [9] のモデルで活性と安全性の性質が成が 0 だったものだけを検査することになり，やはり Travkin

り立つかどうかで判断した．3.5.2 節，問題 3.1，問題 3.7，

らの TSO と PSO の範囲を超えない．以上より，本ライブ

Dijkstra は共有変数に 0 以外の初期値を設定する必要のあ

ラリのモデル化は Travkin らの TSO や PSO の説明に沿っるモデルのため，これらのモデルを検査することで，INITている．

の正しさを調査する．性能の評価は，使用した総メモリ使

6. 実験

用量（一つの状態を表すのに使用したバイト数と状態数を掛け合わせたもの）と実行時間の観点から行った．

本ライブラリが提供するマクロを使用して， ライブラリ

表 1 のモデルと 表 2 のモデルについて，LTL 式を使用

が正しく実装できているかどうかの調査と，共有変数を参して検査した．本ライブラリを使用しない検査では， 表 1

照する LTL 式を使用した検査が正しくできるかどうかののモデルは文献 [16] の記載されているそのままのモデル

調査，その性能の評価を行った．
ライブラリが正しく実装できているかどうかは文献 [15]を，表 2 のモデルは通常の Promela で記述したモデルを検査した．本ライブラリを使用した検査では，表 1 と 表 2112017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日のモデルを，本ライブラリを使用するように変更したモデめにフェンス命令を挿入したことがわかる*5 が，モデル例

ルを検査した．

には PSO で検査する際にフェンス命令を挿入する箇所が

表 1 と 表 2 の「モデル名」の項目のそれぞれの名称の示されていなかった．そこで，PSO で相互排除が成り立つ

後に，活性を検査した場合は (L) を，安全性を検査した場

ように Peterson のモデル例にフェンス命令を挿入したモ合は (S) を記した．表 1 のモデルについては，文献 [16] にデルを検査し，その結果を Peterson∗ に示した．Peterson∗

記載されていた LTL 式を使用して検査を行った．表 2 のでは PSO でも安全性が満たされ，相互排除が成り立つこ

モデルについては，クリティカルセクションを表すラベルとを確認した．

CS を追記して LTL 式による検査を行った．例えば，プロ

以上より，本ライブラリが提供するマクロを使用して，

セス P の活性を検査する際，P が共有変数 F を 1 にしてク

共有変数を参照する LTL 式を使用した検査が正しくでき

リティカルセクションに入ることを表明するならば，以下ることが示せた．

のような式を記述した．

[] ((SVAR(P, F) == 1) -> <> P@CS)

表 1 の「メモリ」と「実行時間」の項目に，それぞれのモデルを検査した際に要した総メモリ使用量（KB）と実

また，活性を検査する際には，-f オプションを付けて弱い

行時間（秒）を示す．ただし，これらの結果は SPIN が反公平性の下でモデル検査を行った．

例を検出するか，反例を検出せずに検査を終了するまでにこのとき，ライブラリのパラメタのうち PROCSIZE と要した総メモリ使用量と実行時間である．

VARSIZE については，各モデルのユーザプロセスの数やグローバル変数の数に合わせて定義した．モデルの中には，どのモデルのどのメモリモデルも，文献 [16] や文献 [9]のモデル以上のメモリと実行時間を要した．

書き込みを含みかつ繰り返しの回数が一定ではないユーザ

例えば，問題 2.1 のモデルの活性を PSO で検査した際プロセスを含むものがあるため，BUFFSIZE はどのモデルは，通常の Promela で記述された文献 [16] のモデルの 1000でも 5 と定義した．さらに， 表 2 のモデルを TSO と PSO

倍以上のメモリを要した．これは， 表 1 の問題 3.1 以外ので検査する際は，文献 [9] に載せられているモデル例の通他のモデルでは一つのユーザプロセスが一つの共有変数にりに，それぞれのメモリモデルで相互排除が成り立つよう

対してのみ書き込みを行っていたのに対し，問題 2.1 のモにフェンス命令を挿入した．

デルでは二つの共有変数に対して書き込みを行ったことが実験に使った環境は，Ubuntu 16.04.2 LTS，Intel Core

i7-6700K 4.00GHz である．

原因だと考えられる．PSO では，各ユーザプロセスは共有
変数毎のストアバッファを持っているため，一つのユーザプロセスが複数の共有変数を操作するモデルでは状態数が6.2 実験結果大きく増えることになる．対して，一つのユーザプロセス

表 1 の SC については，どのモデルを検査した結果も文が一つの共有変数のみを操作するモデルでは，各ユーザプ

献 [16] の結果と一致した．TSO と PSO については，活性ロセスの持つストアバッファのうち一つのストアバッファと安全性を検査した結果が文献 [16] と異なっていたが，こしか使用されないため，TSO と同程度の状態数になる．

れらのモデルは実行順序が緩和されているメモリモデルで問題 3.1 のモデルについては，PSO では状態数が大きくは相互排除が成り立たないアルゴリズムのモデルのため妥なり過ぎたために 47GB のメモリを使用した時点で検査を当であると考えられる．3.5.2 節のモデルはユーザプロセス

打ち切った．その原因は，問題 3.1 のモデルは一つのユーの数が一つのためメモリモデルの影響を受けないが，TSO

ザプロセスが多数の共有変数へ書き込みを行ったことだとと PSO で検査した結果が文献 [16] と一致したため，TSO

考えられる．前述したように，PSO ではユーザプロセス毎と PSO のマクロの実装が単一のユーザプロセスしか持たかつ共有変数毎のストアバッファを持つため，一つのユーないモデルでも正しく動作することが確認できた．問題

ザプロセスが複数の共有変数へ書き込むモデルでは TSO

3.1 もユーザプロセスの数が一つのモデルであり，TSO でよりも状態数が増える．問題 3.1 は一つのユーザプロセス

文献 [16] の結果と一致することを確認した．しかし，PSO

が 6 つの共有変数へ書き込むモデルである．二つの共有変では状態数が大きくなり過ぎたために 47GB のメモリを使数へ書き込む問題 2.1 のモデルでも通常の Promela のモデ用した時点で検査を打ち切った．

ルの 1000 倍以上のメモリを要したことを考えると，問題

表 2 のモデルの活性については，SC で検査した結果は3.1 のモデルの検査には膨大なメモリと実行時間がかかる

通常の Promela で作成したモデルを検査した結果と一致しことが予想され，実際にそのような結果が得られた．なお，た．安全性については，Peterson のモデル例を PSO で検問題 3.1 のモデルのように，ユーザプロセスが一つのモデ査した場合に満たされなかった．文献 [9] の記述を確認しルでは，どのメモリモデルでも通常の Promela で記述したたところ，実験の際に PSO で相互排除を成り立たせるたモデルと実行結果は変わらないはずのため，本ライブラリ*5

p. 16112

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

表 1

モデル検査の教科書のモデルをモデル検査した結果

Table 1 Results of model checking for models in a textbook on model checking.
結果
文献
モデル名

SC

TSO

PSO

メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）

3.5.2 節

46.5

0

129.6

0

4210.40.02

4991.50.02

練習 2.2

0.2

0

0.3

0.01

24.9

0.07

26.1

0.07

問題 2.1(L)

1.7

0

5.0

0.11

130.6

0.02

1914.00.02

問題 2.1(S)

2.7

0

2.5

0.02

5.3

0.13

8.8

0.13

問題 3.1

0.8

0

1.8

0

1477.4

0.01

>47GB

>42.6

問題 3.3

1.9

0

2.3

0

150.0

0.07

146.3

0.07

問題 3.7(L)

1.5

0

2.0

0

251.6

0.13

176.4

0.13

問題 3.7(S)

0.8

0

1.1

0.03

36.9

0.06

25.9

0.06

表 2 メモリモデルを考慮したモデルをモデル検査した結果

Table 2 Results of model checking for intended to run correctly
under the memory models.
結果
文献
モデル名

SC

TSO

PSO

メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）メモリ（KB）

実行時間（秒）Burns(L)

5.8

0

5.8

0

719.3

0.03

710.5

0.03

Burns(S)

2.9

0

2.9

0

369.0

0

364.5

0

Dekker(L)

17.3

0

17.3

0

1929.10.08

4084.20.08

Dekker(S)

8.9

0

8.9

0.01

981.8

0.01

2069.20.01

Dijkstra(L)

8.2

0

8.2

0.03

89.4

0.04

113.7

0.04

Dijkstra(S)

16.2

0

16.2

0

1365.30.03

2216.40.03

Lamport Bakery(L)

2.6

0

2.6

0

25.9

0.12

42.0

0.12

Lamport Bakery(S)

41.9

0

41.9

0

2002.60.01

3235.20.01

Lamport Fast(L)

15.5

0

15.5

0.05

396.5

0.05

237.7

0.05

Lamport Fast(S)

37.7

0

37.7

0.1

3230.20.03

5652.80.03

Peterson(L)

5.4

0

5.4

0

214.0

0.03

601.6

0.01

Peterson(S)

2.8

0

2.8

0

113.7

0

184.0

0

Peterson∗(L)

-

-

-

-

-

-

270.9

0.03

Peterson∗(S)

-

-

-

-

-

-

143.6

0

Szymanski(L)

9.4

0

9.4

0

1732.00.03

1752.2

0.03

Szymanski(S)

5.2

0

5.7

0.01

1098.70.02

1111.50.02

を使用せずに検査できる．

の方が少ないメモリ使用量で検査を終えているが，TSO よ以上より，本ライブラリは，一つのユーザプロセスが多りも PSO の方が一つの状態を表すのに必要なバイト数がくの共有変数へ書き込むモデルでは PSO に従った実行を大きく，状態数が少なかったことから，PSO では TSO で検査する際に状態数が爆発する，という特徴を有すること緩和されていないストア → ストアの実行順序が緩和されがわかる．なお，本ライブラリと同様に，ストアバッファていることによって，早期に活性が成り立たないことを検を用いて共有変数への書き込みを遅延させるアイデアに出したと考えられる．

よって PSO を実現している手法 [13], [14] も同じ特徴を有していると考えられる．
一方，問題 3.7 のモデルを検査した際に使用したメモリ
は，TSO より PSO の方が少なくなっていた．このモデ
ルでは一つの状態を表すのに必要なバイト数が TSO より

PSO の方が少なくなっていた．これは，TSO の実装で必要な各プロセス毎のカウンタが PSO では不要なことや，実行時間については，ほとんどのモデルで SPIN で計測できる最短の 0.01 秒より短く，問題 3.1 以外の最も長いモ
デルで 0.13 秒であった．

7. 関連研究
本研究以前にも，SPIN でメモリモデルに従った実行を検査する手法が提案されている [13], [14], [17]．

TSO ではストアバッファにメモリアドレスと値の組を格Wehrheim らは，C/C++のコードを LLVM の IR コー

納しているのに対して PSO では値のみを格納しているこドを介して TSO，PSO に従った動作をする Promela コーとが原因である．ユーザモデルによっては PSO のモデル

ドに変換する手法を提案している [13], [14]．この手法は，のサイズが TSO よりも小さくなることがある．表 2 の本研究の手法と同じく，ストアバッファによって TSO と

Lamport Fast のモデルを検査した場合も，TSO より PSO

PSO で起こり得るメモリアクセス命令の実行順序の入れ13

2017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

替わりを表現するアイデアによるものである．Wehrheim

した．

らの手法では通常の Promela と同様に，LTL 式と assert

改良したライブラリを実装し，実験を行った結果，改良文によって検査した性質を記述する．LTL 式内からどのしたライブラリが提供するマクロの動作が正しいことを確

グローバル変数の値でも参照できるが，参照できるのは実認した．性能の評価を行った結果，本ライブラリは一つの際にメモリに反映された値のみで，本研究の手法が提供すユーザプロセスが多くの変数へ書き込むモデルでは PSO

る SVAR 命令のような，ある特定のプロセスが観測できるに従った実行を検査する際に状態数が爆発する，という特グローバル変数の値を参照することができない．本研究徴を有することが示された．実行時間については，検査をの手法では，実際にメモリに反映された値だけでなく，あ打ち切ったモデル以外の実験では，現代の計算機で十分実る特定のプロセスが観測できるグローバル変数の値も参行可能な実行時間で検査を完了した．

照できる．また，Wehrheim らの手法によって生成される

今後の課題としては，まず，本ライブラリと関連研究とPromela コードは可読性が低いにも関わらず，検査したい

して紹介した Wehrheim らのライブラリ [13], [14] で TSO性質を記述するためにはそのコードを読む必要がある．本と PSO の動作に違いがあるかどうかの調査が挙げられる．

研究の手法では，メモリモデルを考慮しないモデル内の共

他にも，これまでに扱わなかったメモリモデルへの対応や，有変数に対するメモリアクセス命令を，ライブラリが提供

キャッシュコヒーレンシを考慮したモデルの開発が挙げらするメモリアクセス命令にほとんど置き換えるだけで TSOれる．また，ライブラリのパラメタのうちプロセスの数とと PSO に従った実行を検査できる．そのため，コードの共有変数の数についてはユーザの責任としているが，これ可読性が高く，検査したい性質を容易に記述できる．

らを検査対象のプログラムから自動的に抽出する仕組みを

Wehrheim らは，SC，TSO，PSO に従った実行を検査開発することは，ライブラリの使いやすさのためには急務できる Promela で記述されたライブラリを，[13], [14] でである． 本ライブラリでは書き込みがストアバッファか実験の比較対象として使用している．このライブラリは，ら溢れるとブロックするが，ストアバッファから溢れると本研究と同じく，ストアバッファを用いたアイデアによっエラーとする手法も存在する [13], [14]．エラーにする方がて実装されている．しかし，Wehrheim らのライブラリでユーザは正しく検査できていないことを認識しやすいが，は，グローバル変数がユーザから隠されているため，我々本ライブラリでは有界モデル検査で使用することも考えてが以前に開発したライブラリと同様にグローバル変数を参ブロックするように実装した．今後，エラーにする機能も照した LTL 式を記述できない．改良したライブラリでは，追加して拡張したい． さらに，本ライブラリでは CAS

ユーザが共有変数（複数のプロセスがアクセスする場合の命令のような CPU 毎にセマンティクスが異なる命令を提あるグローバル変数）にアクセスできるように，専用のマ

供していない．本ライブラリが提供するマクロと Promela

クロを提供することで，Wehrheim らのライブラリの欠点の機能を組み合わせることでユーザが定義できる命令もあを克服している．

るがそうでないものもあるため，代表的な命令が定義でき

Tomasco らは，メモリモデルに従った動作をする APIを設計し，CBMC[7] や Nidhugg[1] をバックエンドとして利用して，メモリモデルに従ったモデル検査を提供しているように改良することも今後の課題である．
謝辞

本 研 究 の 一 部 は ，JSPS 科 研 費 16K21335 と16K00103 の助成を受けたものです．

る [12]．しかし，Tomasco らの手法では LTL 式による検査をサポートしていない．

Abdulla らは，ステートレスモデル検査によるメモリモデ

参考文献
[1]

ルを扱えるモデル検査器を提案している [1], [2]．Abdullaのモデル検査器は C で記述されたマルチスレッドプログラ
ムのみを対象としているが，本研究の手法では Promela で[2]モデル化することで C 以外のマルチスレッドプログラムも検査できる．

[3]

8. おわりに
本論文では，我々が開発してきた，SPIN で弱いメモリ[4]

モデルに従った実行を検査できるようにするためのライブ
ラリを改良した．具体的には，まずガードからも共有変数を参照できるように改良した．さらに，共有変数の初期値を設定できるように改良した．最後に，検査したい性質をLTL 式で記述する際に共有変数を参照できるように改良[5]Abdulla, P. A., Aronis, S., Atig, M. F., Jonsson, B.,
Leonardsson, C. and Sagonas, K. F.: Stateless Model
Checking for TSO and PSO, Proc. of TACAS, LNCS,
Vol. 9035, pp. 353–367 (2015).
Abdulla, P. A., Atig, M. F., Jonsson, B. and Leonardsson, C.: Stateless Model Checking for POWER, Proc. of
CAV, LNCS, Vol. 9780, pp. 134–156 (2016).
Abe, T. and Maeda, T.: A General Model Checking
Framework for Various Memory Consistency Models,High-Level Parallel Programming Models and Supportive Environments, pp. 332–341 (2014).
Adve, S. V. and Gharachorloo, K.: Shared memory consistency models: a tutorial, IEEE Computer, Vol. 29,
No. 12, pp. 66–76 (1996).
Clarke, E. M., Emerson, E. A. and Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM TOPLAS, Vol. 8,
No. 2, pp. 244–263 (1986).

142017-2-(1): 情報処理学会プログラミング研究会 発表資料 2017 年 7 月 28 日

[6]
[7]

[8]

[9]
[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

Holzmann, G. J.: The SPIN Model Checker, AddisonWesley (2003).
Kroening, D. and Tautschnig, M.: CBMC - C Bounded
Model Checker - (Competition Contribution), Proc. of
TACAS, LNCS, Vol. 8413, pp. 389–391 (2014).
Lamport, L.: How to Make a Multiprocessor Computerthat Correctly Executes Multiprocess Programs, IEEE
TC, Vol. C-28, No. 9, pp. 690–691 (1979).
Linden, A.: On the Verification of Programs on Relaxed
Memory Models, PhD Thesis, Universite de Liege (2013).
Linden, A. and Wolper, P.: An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models, SPIN, LNCS, Vol. 6349, pp. 212–226 (2010).
Owens, S., Sarkar, S. and Sewell, P.: A better x86 memory model: x86-TSO (extended version), Technical Report UCAM-CL-TR-745, University of Cambridge, Computer Laboratory (2009).
Tomasco, E., Nguyen, T. L., Inverso, O., Fischer, B.,
Torre, S. L. and Parlato, G.: Lazy Sequentialization for
TSO and PSO via Shared Memory Abstractions, Proc.
of FMCAD (2016).
Travkin, O. and Wehrheim, H.: Verification of Concurrent Programs on Weak Memory Models, Proc. of ICTAC, LNCS, Vol. 9965, pp. 3–24 (2016).
Wehrheim, H. and Travkin, O.: TSO to SC via Symbolic
Execution, Proc. of HVC, LNCS, Vol. 9434, pp. 104–119(2015).
松元稿如，鵜川始陽，安部達也：メモリモデルを考慮したメモリアクセス命令を提供する SPIN 用ライブラリ，ソフトウェア工学の基礎，Vol. 23, pp. 63–72 (2016).
産業技術総合研究所システム検証研究センター：モデル
検査 上級編−実践のための三つの技法−，株式会社近代科学社 (2010).
加藤寿和，一場利幸，本田晋也，高田広章：ハードウェ
アの振舞いを考慮したスピンロックのモデル検査，研究
報告組込みシステム（EMB），Vol. 2011, No. 2, pp. 1–8(2011).

安部 達也 （正会員）
1979 年生．2002 年京都大学理学部卒
業．2007 年東京大学大学院情報理工学系研究科博士後期課程退学．同年産
業技術総合研究所システム検証研究センターテクニカルスタッフ．2008 年
同センター特別研究員．2009 年京都大学学術情報メディアセンター特定助教．2011 年理化学研究所計算科学研究機構特別研究員．2013 年同機構研究員．

2015 年千葉工業大学人工知能・ソフトウェア技術研究セン
ター上席研究員，現在に至る．博士 (情報理工学)．プログ
ラミング言語の理論と実装，プログラム検証の研究に従事．

松元 稿如
1994 年生．2017 年高知工科大学情報学群卒業．2016 年 IEEE Computer

Society Japan Chapter FOSE Young
Researcher Award 受賞．

鵜川 始陽 （正会員）
1978 年生．2000 年京都大学工学部情報学科卒業．2002 年同大学大学院情報学研究科通信情報システム専攻修士課程修了．2005 年同専攻博士後期課
程修了．同年京都大学大学院情報学研究科特任助手．2008 年電気通信大学
助教．2014 年より高知工科大学准教授．博士 (情報学)．プ
ログラミング言語とその処理系に関する研究に従事．情報処理学会 2012 年度山下記念研究賞受賞．

15