2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

SPIN によるメモリ順序を考慮した
ソフトウェアモデル検査の反例可視化
松元 稿如1,a)

鵜川 始陽1,b)

概要：現代のプロセッサでは，メモリアクセス命令がプログラムに記述された順序（プログラム順序）と，それがメモリに反映される順序（メモリ順序）が異なることがある．そのため，並行プログラムの検査では，プログラム順序だけでなくメモリ順序を考慮する必要がある．これまでに我々は，モデル検査器 SPINを使って，メモリ順序を考慮したモデル検査を行うためのライブラリ MMLib を開発した．SPIN は，命令型のモデル記述言語 Promela で記述したプログラムのモデルを入力とする．モデル検査によりバグが見つかった時は，Promela で記述したモデル上のエラーに至る実行トレースである反例を読み解くことになる．
しかし，MMLib を使用したモデルの反例では，メモリ順序が MMLib が内部的に使う変数の値からしか分
からず，読み解くのが難しい．そこで我々は，MMLib を使用したモデルの反例を可視化するソフトウェアを開発した．このソフトウェアは反例に沿ってモデルの実行を再現する．その時に， メモリに反映されていないメモリアクセス命令をハイライト表示し，メモリ順序が分かるようにする．¿¿¿¿¿¿¿ master2
キーワード：SPIN，メモリモデル，モデル検査，デバッグ，可視化

Visualization of Counterexamples ofMemory Model-Aware Software Model Checking Using SPIN
Kosuke Matsumoto1,a)Tomoharu Ugawa1,b)

Abstract: In modern processors, the memory order, which is the order of memory access operations reflected to the memory, is not necessarily the same as the program order, which is the order of memory accessinstructions listed in the program. Thus, when we verify concurrent programs, we have to take the memoryorder into account. In our previous work, we developed a model checking library, MMLib, which helps us
conduct model checking with taking the memory order into account using the SPIN model checker. The
input of SPIN is a model of the program written in Promela, an imperative style modeling language. When
SPIN reports an error, the user of SPIN has to understand the counterexample, which is the execution traceon the model written in Promela resulting in the error. However, counterexamples of models written using
MMLib are diﬃcult to understand because we need to interpret the values of variables used internally in
MMLib. Therefore, we developed a software to visualize counterexamples of models using MMLib. The
software visualizes the execution of the model step by step along a counterexample. In the step execution,
it highlights memory access instructions that have been executed but yet to be reflected to memory tovisualize the memory order.
Keywords: SPIN, memory model, model checking, debug, visualization

1. はじめに1a)b)

高知工科大学
Kochi University of Technology, Kami, Kochi 782–8502,
Japan
matsumoto@pl.info.kochi-tech.ac.jp
ugawa.tomoharu@kochi-tech.ac.jp

並行プログラムのモデル検査では，メモリアクセス命令
がプログラムに記述された順序（プログラム順序）だけでなく，それがメモリに反映される順序（メモリ順序）も考1

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

慮する必要がある．現代のプロセッサでは，プログラム順

実行ステップについて以下の情報が必要であった [4], [5]．

序とメモリ順序が異なる場合がある．その結果，プログラ(1) グローバル変数やローカル変数のメモリ上の値と，各ム順序通りにメモリアクセス命令がメモリに反映されればスレッドから見える値．

正しく動作するプログラムでも，メモリ順序によってはエ(2) 各スレッドが実行したメモリアクセス命令のうち，メラーが発生する場合がある．これは，命令を実行したのとモリに反映されていないメモリアクセス命令．

は別のスレッドからは，命令がメモリ順序で実行されたよ

そこで我々は，MMLib を使用したモデル検査の反例をうに見えるからである．命令がどんなメモリ順序で実行さ可視化し，上記の情報をユーザに提示できるソフトウェア

れることがあるか定義したものをメモリモデルと呼ぶ．

を開発する． 本ソフトウェアは，反例に沿ってモデルの実

これまでに我々は，モデル検査器 SPIN を使いメモリモ

行を再現し，モデル上に視覚的に上記の情報を提示する．

デルを考慮してプログラムをモデル検査するためのライブ

本反例可視化ソフトウェアは，一般的な命令型言語のデラリ MMLib を開発した [1], [2]．MMLib は，SPIN[3] のモバッガと同様に，モデルの文単位や行単位でステップ実行

デル記述言語 Promela で記述されたモデルの部品である．

の様子を表示する．さらに，まだメモリに反映されていなプログラムのモデルと MMLib を結合して SPIN に入力すいメモリアクセス命令や，プログラム順序とメモリ順序がることで，メモリモデルを考慮したモデル検査を行える．

異なったメモリアクセス命令をハイライト表示する．

MMLib は，プログラム順序とメモリ順序が異なること

本論文では，まず 2 章で例を用いて MMLib を使ってデに起因するバグの発見とデバッグに用いることを想定してバッグする際の問題点を挙げる．次に，??章で MMLib のいる．このユースケースでは，プログラム順序での実行で内部構造を説明する．その後，3 章で本反例可視化ソフト

はエラーが起きないことを他のツールなどを使って確かめ

ウェアの設計を説明 する．4 章で本反例可視化ソフトウェ

た後に，MMLib を用いたモデル検査を行う．そのため，本アを使ったデバッグとバグの理解の事例を示し，5 章で既研究でも，MMLib を使ったモデル検査の対象は，プログ存の反例可視化ソフトウェアと比較する．さらに，6 章で

ラム順序の実行ではエラーが起きないことを仮定する．

関連研究について言及し，7 章で本論文のまとめと今後のSPIN のモデル記述言語 Promela は命令型の言語である．
SPIN は，Promela で記述されたモデル中の各スレッド*1 をインタリーブしながら 1 文ずつ順に実行した時に，エラーに至る可能性があるかどうかを検査する．エラーに至る可
能性はバグである．バグが見つかった時は，モデル上のエラーに至る実行トレースである反例を出力する．

課題を述べる．

2. MMLib を使ったデバッグの問題
2.1 ピーターソンの相互排除アルゴリズム
図 1 はピーターソンの相互排除アルゴリズム [6] のプロ
グラムである．ピーターソンの相互排除アルゴリズムは，モデル検査を利用してプログラムをデバッグする場合，

メモリアクセス命令がプログラム順序通りにメモリに反映

ユーザは反例からバグの原因を読み解く必要がある．しかされることを仮定している．その仮定が成り立たないメモ

し，MMLib を使用したモデル検査の反例は次の二つの理リモデルでは排他制御ができない．

由から読み解くのが難しい．一つ目は，反例中に MMLib

関数 T0 と T1 は異なるスレッドで実行されることを想の内部的な実行ステップが含まれるためである．MMLib

定しており，Critical Section というコメントが排他制

はプログラムのモデルと同じく Promela で記述されている御の対象となるクリティカルセクションである．共有変数

ため，SPIN は MMLib の内部のモデルの実行とプログラム

want0 と want1（以下，まとめて want と書く）は，それぞのモデルの実行とを区別せず反例を出力する．そのため，

れ T0 と T1 を実行するスレッドがクリティカルセクション

ユーザが反例の実行ステップとプログラムのモデル上の行に入りたいという表明である．クリティカルセクションにとの対応を取るのは難しい．二つ目は，メモリアクセス命

入りたいスレッドはそのスレッドの want を 1 にする．そ令がどのようなメモリ順序で実行されたのかは，MMLibの後，他方のスレッドの want を読んで，0 であればクリの内部的な変数の値から読み解く必要があるためである．

ティカルセクションに入れる．他方の want を読むのは自

この二つの理由のうち，前者は MMLib に限らず，同様の

身の want を 1 にした後なので，両方のスレッドが同時にマクロを使ったモデル検査ライブラリにも共通する．後者

クリティカルセクションに入ることはない．しかし，これは，メモリ順序を考慮したデバッグ特有である．本論文でだけでは両方のスレッドが同時に自身の want を 1 にしては後者に焦点を絞り，メモリ順序を可視化する方法を提案

デッドロックする可能性がある．turn はそれを解決する

する．

ための変数である．

我々の経験では，メモリモデルを考慮したモデル検査によって，プログラムのバグを理解しデバッグするには，各2.2 MMLib を使った Promela モデル
図 1 のプログラムのモデルを MMLib を使って Promela*1

Promela ではプロセスと呼ぶ．

で記述すると図 2 のようになる．Promela ではスレッド

2

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日の定義に proctype というキーワードを使う．図 1 の関数 1T0 と T1 は図 2 の T0 と T1 に対応している．図 2 の 38 行 2# include < pthread .h >目にある ltl キーワードの行は，両方のスレッドが同時に 3

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

クリティカルセクションに入ることはないという仕様を線4形時相論理式 (LTL 式 ) で記述したものである．SPIN は

5

この仕様を満たさない実行トレースを探す．

void * T0 () {6

want0 = 1;

7

turn = 1;

Promela のモデル中で，複数のスレッドからアクセスさ 8れる変数（共有変数）にアクセスするには MMLib を使う． 9

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

MMLib は共有変数を管理しており，共有変数にアクセス 10

break ;

するマクロを提供している．つまり，共有メモリとメモリ 11
アクセス命令は，MMLib では，共有変数と共有変数アクセ/* Critical Section */12

want0 = 0;13

return 0;

ス命令としてモデル化されている．MMLib は，共有変数 14}

アクセス命令として共有変数 x から値を読み出す READ(x) 15
や，x に値 v を書き込む WRITE(x, v) に加えて，プログラ 16

void * T1 () {ム順序で先行する命令と後続の命令が反映される順序を強 17

want1 = 1;

制するためのフェンス命令のマクロ FENCE() を提供して 18

turn = 0;

いる．

19

while ( true )20

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

MMLib では共有変数は整数で識別するため，WRITE の 21

break ;

第一引数には共有変数を識別する整数を渡す必要がある．22/* Critical Section */図 2 では，Promela で C 言語のマクロが使用できることを 23

want1 = 0;

利用して，5 行目から 7 行目のように変数名を表すマクロ 24を定義している．これにより，WRITE の第一引数に変数名 25を渡せるようにしている．例えば，共有変数 turn に 1 を書き込むには，11 行目のように WRITE(turn, 1) と記述する．同様に，turn の値を読み出すには，13 行目のようにREAD(turn) と記述する．

return 0;}

図 1: ピーターソンのアルゴリズムによる相互排除プログラム
Fig. 1 Program of Peterson’s mutual exclusion program

で議論に登場しない部分を省略している．我々の過去の研2.3 エラーの原因究 [5] では，この反例を読み解いてバグを理解していたが，図 2 のスレッド T0 がクリティカルセクションに入るた

それには MMLib の内部構造に関する知識が必要になり，

めには，12 行目の if 文のいずれかの条件が真になる必要知っていたとしても難しい． 以下では図 3 から，メモリがある．Promela では，条件分岐は if と fi を使って記述順序に関連したバグを理解するのに必要になる情報を読みする．if 文では，非決定的選択を表す “::” のうち後に続解く方法を示す．

く条件が真である分岐が非決定的に実行される．そのよう

2.4.1 アクセスしている共有変数の値

な分岐がなければ，いずれかの条件が真になるまで，そのスレッドの実行がブロックする．
ここでは 14 行目でスレッド T1 がクリティカルセクショ

READ や WRITE が アクセスする共有変数の値は，MMLibが内部的に使う複数の変数の値に依存する． 例えば，図 3 の反例の 14 行目は，図 2 の 14 行目の READ(want1) に対応してンに入る表明である want1 を読み出している．スレッド T1

いる．この READ で読み出される値は，反例の 2 行目から 13

が 21 行目で WRITE(want1, 1) を実行した瞬間に，その結果

行目の buffer や lcounter，shared memory に依存する．

が共有変数を介してスレッド T0 の 14 行目の READ(want1)

この例では lcounter[7] が 0 なので，shared_memory[1]で読み出せるようになっていれば，スレッド T0 は if 文での値である 0 が読めている． ここで，配列インデックスのブロックされ，相互排除ができる．しかし，WRITE が共有

1 は変数 want1 を識別する整数であり，7 はそこから計算

変数に反映されるのが遅れると，want1 が 0 のままの状態される値である．

が観測でき，スレッド T0 がクリティカルセクションに入っ

2.4.2 未反映の WRITEてしまう．

共有変数に反映されていない WRITE は，MMLib 内部のキューに保存されている． 図 3 の反例の 16 行目から 20

2.4 反例行目の queue は実行されたが共有変数にはまだ反映されて

図 2 のモデルを検査し，SPIN が出力した反例から一部

いない WRITE を格納するキューで，19 行目の [1] は T1 がを抜粋したものを図 3 に示す．ただし，スペースの都合実行した WRITE(want1, 1) を表している．図 2 の 14 行目

32018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

ユーザに提示する．

1# define PROCSIZE 2

2# define VARSIZE 3

3# define BUFFSIZE 5

4# include " pso . h "本反例可視化ソフトウェアは Eclipse のプラグインとして

5# define want0 0

実装する．

6

# define want1 ( want0 + 1)

7

# define turn(2) 共有変数アクセス命令がアクセスする変数の値を提示する．

( want1 + 1)

3.1 反例可視化ソフトウェアの機能

89

本反例可視化ソフトウェアは，命令型プログラミング言

proctype T0 () {WRITE ( want0 , 1);

語の GUI デバッガと同じように，モデル上の実行を 1 ス

11WRITE ( turn , 1);

テップずつ表示することで反例を可視化する．反例可視化

12

if

13

::( READ ( turn ) == 0)

14::( READ ( want1 ) == 0) -> skip ;

15

fi ;

10

16

図 4 は本反例可視化ソフトウェアを用いて図 2 のモデルで見つかったエラーの反例を表示している様子である．

WRITE ( want0 , 0);}

本反例可視化ソフトウェアは，操作ビューやモデルビュー

1920

しか表示しない．反例可視化ソフトウェア上に表示されている実行ステップを現在の実行ステップと呼ぶことにする．

CS : skip ; /* Critical Section */17
18

ソフトウェア上には，同時には一つの実行ステップの情報-> skip ;と，変数表示ビューから構成されている． 変数表示ビュー
proctype T1 () {21には，共有変数の値を表示する共有変数ビューと，図 4 にWRITE ( want1 , 1);

22

WRITE ( turn , 0);は表示していないが，ローカル変数の値を表示するローカ

23

if

ル変数ビューがある． 操作ビューにはモデルや反例を読み

24::( READ ( turn ) == 1)-> skip ;込むための機能や現在の実行ステップを切り替えるための25::( READ ( want0 ) == 0) -> skip ;ナビゲーションボタンが配置されている．モデルビューに

26

fi ;

は，ユーザが作成したプログラムのモデルが表示され，そ27

CS : skip ; /* Critical Section */28
29

WRITE ( want1 , 0);}

共有変数に未反映の WRITE などの情報が表示される．

init {

応して次の機能を持つ．

本反例可視化ソフトウェアは，上記の要件 (1)，(2) に対

30
31
32

atomic {33

run T0 ();34

run T1 ();

35
36

}

(1) 未反映 WRITE 命令ハイライト機能(2) 各スレッドから観測できる共有変数の値の表示機能
3.1.1 未反映 WRITE 命令ハイライト機能
いずれかのスレッドによって実行はされたが，現在の実}行ステップではまだ共有変数に反映されていない WRITE 命

3738の上に現在の実行ステップでの各スレッドの実行位置や，

ltl prop {! <> ( T0@CS && T1@CS )}

令を，モデルビュー上で黄色にハイライトする．MMLibを使ったモデル検査が対象とするのは，プログラム順序で

図 2: MMLib を使用した図 1 のプログラムの Promela モ
デルFig. 2 Promela model for the program in Fig.1 with MMLibの実行ではエラーが起きないプログラムのモデルなので，本反例可視化ソフトウェアを使って理解しようとするバグ
はメモリ順序に起因するバグである．未反映の WRITE 命令
はメモリ順序が確定しておらず，バグを理解するうえで注で want1 から 0 が読み出される原因が，この WRITE の結果が共有変数に反映されていないためであると理解するには，このように読み解く必要がある．

3. 反例可視化ソフトウェア

意する必要がある．
さらに，次のどちらかの条件を満たす WRITE はバグの原因になり得るので，該当の実行ステップでは，モデルビュー
上で該当の WRITE を赤色にハイライトする．
条件 a.

共有変数アクセス命令 M （WRITE 命令や READ 命

ユーザが反例を読まずともバグを理解できるようにする

令）が共有変数に反映された実行ステップで，プログことを目的として，反例可視化ソフトウェアを開発する．

ラム順序で M に先行するが共有変数に未反映で残っ本反例可視化ソフトウェアの具体的な要件は次の二つでている WRITE 命令 W0 ．

ある．

(1) WRITE が共有変数に反映されたタイミングを視覚的に

条件 b.

共有変数 x を対象とした READ 命令が共有変数に反映された実行ステップで，他のスレッドが実行し42018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

1

19: proc 2 ( T0 :1) peter . pml :11 ( state 16) [ temp = 0]2

shared_memory [0] = 0

3shared_memory [1] = 0

4shared_memory [2] = 0

5

...

6

buffer [6] = 1

7

buffer [7] = 0

8buffer [8] = 1

9

...

10

lcounter [6] = 1

11lcounter [7] = 0

12lcounter [8] = 1

13

...

14

21: proc 2 ( T0 :1) peter . pml :14 ( state 21) [((( (( lcounter [(( _pid *3)+1)]==0)) ->15( shared_memory [1]) : ( buffer [(( _pid *3)+1)]) )==0))]16

queue 1 ( queue [0]):

17

...

18

queue 10 ( queue [9]):19queue 11 ( queue [10]): [1]20queue 12 ( queue [11]): [0]図 3: 図 2 の反例の一部
Fig. 3 A part of counterexample of Fig.2.

た同じ共有変数 x を対象とする共有変数に未反映のが表示される．これは共有メモリ上の値とは異なることがWRITE 命令 W1 のうち，後続のいずれかの共有変数ア

あるが，READ 命令の実装と同じ計算をすることで，MMLib

クセス命令は共有変数に反映されているもの．

が内部的に用いる変数から再現できる．

条件 a では，この実行ステップで，M と W0 がメモリ順

表の 1 列目に共有変数名を表示するには，3.2.2 節で後述

序で入れ替わることが確定するので，バグの原因になり得する共有変数の情報を記述した共有変数情報ファイルで変る．なお，MMLib が扱うメモリモデルでは，READ は実行数名を指定する必要がある．共有変数情報ファイルがなけされると直ちに共有変数に反映される．例えば，図 2 のス

れば，変数名ではなく，変数を識別する整数を表示する．

レッド T1 によって 25 行目の READ(want0) が実行された

本反例可視化ソフトウェアには，共有変数だけでなく，

とき，21 行目の WRITE(want1, 1) がまだ共有変数に反映

ローカル変数を表示するローカル変数ビューもある．ロー

されていなければ，この WRITE を赤色でハイライトする．

カル変数はメモリ順序の影響を受けないので，ローカル変条件 b の W1 は，条件 a によって，それ以前の実行ステッ

数ビューに特別な仕組みは必要ない．

プで一度ハイライトされているはずである．それを改めてハイライトするのは，実際にメモリ順序が入れ替わったこ

3.2 その他の特徴とが他のスレッドに観測されるというイベントが発生する

3.2.1 実行ステップからである．これはバグの原因となり得る．例えば，図 2

SPIN が出力する反例には MMLib の内部的な動作も含まのスレッド T0 によって 14 行目の READ(want1) が実行される．しかし，それらはユーザには必要ないので，ユーザがれたとき，スレッド T1 の WRITE(want1, 1) がまだ共有変記述した MMLib を使う Promela のモデルの視点でのイベ数に反映されておらず，かつ，READ(want0) は実行されてントのみを実行ステップとして表示する．WRITE や FENCE

しまっていれば，この WRITE を赤色でハイライトする．こなどのマクロは，不可分に実行される複数の Promela の文

れは，まさに 2.3 節で述べたエラーの原因になっている．

で構成されているが，これらはまとめて 1 ステップとする．

3.1.2 各スレッドから観測できる共有変数の値の表示機能

また，WRITE は専用のプロセスが不可分に実行する複数の

図 4 の共有変数ビューに示すように，現在の実行ステッ

Promela の文によって共有変数に反映されるので，これもプの各共有変数の名前と値の表を表示する．表の 1 列目にまとめて 1 ステップとする．

は共有変数名を，2 列目には現在の実行ステップでの共有

Promela では，モデルが満たすべきでない性質を記述す

変数の共有メモリ上での値が表示される．3 列目以降には，るために never claim という特別なスレッドを利用できる．

各スレッドが現在の実行ステップで観測する共有変数の値

LTL で記述した仕様も never claim に変換される．never5

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

図 4: 反例可視化ソフトウェア
Fig. 4 Counterexample visualizer.

claim は他のスレッドとは独立して動作し，モデルが満た

表 1: モデルのサイズ

すべきでない性質を満たすと受理ラベルを持つサイクルにTable 1 Sizes of models.

入る．never claim がそのようなサイクルに入ると，SPIN

model

line

threadshared variable

はエラーを検出し反例を出力する*2 ．never claim はプログ

Peterson38

2

3

ラムのモデルではないが，その動作はプログラムのモデル

Staccato

174

2

6

をデバッグする上で重要な意味を持つ．そのため，本反例
可視化ソフトウェアでは反例中の never claim を実行すると，並行ガベージコレクション（GC）の Staccato [7] のアステップも 1 ステップとして扱う．

ルゴリズムを題材に，本反例可視化ソフトウェアを使った

3.2.2 共有変数名

デバッグとバグの理解の方法を述べる*3 ．

MMLib は共有変数を整数値（以下，変数番号）で識別
するが，MMLib を使う Promela のモデル上では通常，記表 1 に，本章で用いたモデルのサイズとして，モデルの行数，スレッド数，および共有変数の数を示す．

号的な識別子を変数番号で定義して用いる． しかし，このような対応を参照しながら反例を理解するのは手間がかか

4.1 バグを理解する方針

る． そこで，ユーザがこの対応を共有変数情報ファイル

次の方針でバグを理解する．まず，短い反例を利用する．

に記述して本反例可視化ソフトウェアに指示することにし

一般に，エラーに至る実行トレースがある場合，それは複た．本反例可視化ソフトウェアは共有変数情報ファイルか数ある．SPIN には，最短のステップ数でエラーに至る実

ら読み取った名前を使って共有変数ビューを表示する．

行トレースを反例として出力する機能があるので，それを4. ケーススタディ活用する．これは，短かい反例の方がバグを理解しやすい

本章では，図 1 のピーターソンの相互排除アルゴリズムからである．ただし，ここで得られる反例は MMLib の内部的な実行ステップも 1 ステップと数えたときに最短な反*3*2

SPIN は Promela のモデルを Büchi オートマトンに変換して探索する．Büchi オートマトンでは受理状態を含むサイクルに入ると入力を受理したことになる．never claim が受理されるとエラーとして扱われる．

ピーターソンのアルゴリズムはプログラム順序とは異なるメモリ順序で実行されるメモリモデルを想定していないので，本当はア
ルゴリズムのバグではなく誤用である．しかし，ここではピー
ターソンのアルゴリズムを，このようなメモリモデルに対応する
ように修正することをデバッグと呼ぶことにする．

6

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

例である．それでも，ユーザが書いた Promela モデル上の反例としても最短な反例の十分な近似になっている．
次に，本反例可視化ソフトウェアが赤色でハイライトする，バグの原因になり得る WRITE に注目する．プログラム
順序では正しく動作するプログラムのモデルを前提としているので，バグの原因は，いずれかの共有変数アクセス命
令でプログラム順序とメモリ順序が入れ替わることに絞られる．そこで，順序が入れ替わった実行ステップで，どの命令が入れ替わったかを可視化する，赤色のハイライトを積極的に利用することにする．
図 5: スレッド T1 がクリティカルセクションに入る実行ス

4.2 ピーターソンによる相互排除アルゴリズム
2 章で述べたように，図 1 のピーターソンの相互排除アテップ
Fig. 5 Execution step in which thread T1 enters the criticalsection.

ルゴリズムでは，プログラム順序とは異なるメモリ順序で実行されると両方のスレッドが同時にクリティカルセク
ションに入ってしまう．以下では，ピーターソンの相互排
除アルゴリズムのモデル（図 2）に対して，本反例可視化
ソフトウェアを使ったデバッグの手順を述べる．

( 1 ) SPIN が出力した最短の反例を本反例可視化ソフト
ウェアにロードして，最初のスレッドがクリティカルセクションに入った実行ステップまで進める．この実行ステップでは，スレッド T1 が図 2 の 25 行目のREAD(want0) == 0 の条件成立によってクリティカルセクションに入っているのが分かる．この実行ステッ
プで，初めて赤色でハイライトされる WRITE が現れた（図 5）．特に，図 2 の 21 行目のスレッド T1 による WRITE(want1, 1) が赤色でハイライトされており，共有変数上ではまだスレッド T1 がクリティカルセク

図 6: スレッド T0 がクリティカルセクションに入る実行ス
テップ
Fig. 6 Execution step in which thread T0 enters the criticalsection.

ションに入ることを表明したことになっていないと分かる．これはエラーの原因になり得る．

( 4 ) 新しい反例を本反例可視化ソフトウェアにロードし( 2 ) さらに実行ステップを進めると，今度はスレッド T0て，実行ステップを進めると図 7 で最初に赤色のマーの実行が進み，スレッド T0 が図 2 の 14 行目の，クカーが表示された．この実行ステップで実行が進んリティカルセクションのガード文 READ(want1) == 0だスレッドは T1 だった．したがって，このハイライを実行する（図 6）．このとき，スレッド T0 が実行しトは図 2 の 21 行目の WRITE(want1, 1) を追い越し

た WRITE だけでなく，スレッド T1 が実行した，図 2て 22 行目の WRITE(turn, 0) が共有変数に反映されの 21 行目の WRITE(want1, 1) も赤色でハイライトさたことを示している．このとき，スレッド T0 の実行れた．これは，スレッド T1 のクリティカルセクショ

した図 2 の 11 行目の WRITE(turn, 1) は黄色にハインに入る表明がスレッド T0 に届かなかったことを表ライトされており，まだ共有変数に反映されていない

している．実際，共有変数ビューで変数 want1 の値をことが分かる．この WRITE(turn, 1) が共有変数に反確認すると 0 のままであった．

映されると，turn は 1 になる．そうすると，スレッ( 3 ) ここまでの理解で，図 2 の 21 行目の WRITE(want1, 1)

ド T1 はいつでもクリティカルセクションに入れるよと 25 行目の READ(want0) の順序が入れ替わることがうになる．一方，スレッド T1 による図 2 の 21 行目

エラーの原因だと分かる．そこで，それを禁止するよの WRITE(want1, 1) はまだ共有メモリに反映されてうに，図 2 の 23 行目の if 文の直前に FENCE 命令をいない．そのため，スレッド T0 もクリティカルセク

挿入する．二つのスレッドは対称なので，スレッド T0

ションに入れる状態にある．実際，この先の実行でスにも同様に FENCE 命令を挿入する．このように修正しレッド T0 がクリティカルセクションに入り，続いてたモデルでモデル検査すると，エラーが報告され新しスレッド T1 が READ(turn) == 1 の条件成立によりクい反例が得られた．

リティカルセクションに入った．

7

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

図 8: Staccato のバグの原因
図 7: 新しい反例で最初に赤色のハイライトが表示される

Fig. 8 Cause of the bug of Staccato.

実行ステップFig. 7 Execution step in which the first red highlight is displayed in the new counterexample.

例では，実行全体で，モデルにある 17 個の WRITE のうちの3 個が，合計で 13 回赤くハイライトされた．その中で，図 8の 2 行目で赤くハイライトされている WRITE(from data,( 5 ) このエラーの原因は，スレッド T1 が共有変数 want1val) がバグの原因だった．この WRITE は，ミューテータ

への WRITE が共有変数に反映される前に turn に書きによる FROM 空間を表す共有変数 from data への書き込

込んでしまったことである．そのため，クリティカルみである．この WRITE の反映が遅れたため，コレクタは新セクションに入ることが可能な状態のスレッド T0 にしい値を観測できず，図 8 の 20 行目の WRITE(to data,

よって turn が上書きされてしまい，スレッド T1 もREAD(from data)) で，from data から古い値を読み出し

クリティカルセクションに入れるようになってしまって TO 空間にコピーしてしまった．これは本反例可視化た．そこで，WRITE の順序が入れ替わるのを禁止する

ソフトウェアで次のように表示されている．コレクタが，ように，図 2 の 21 行目の WRITE(want1, 1) と 22 行

from data から古い値を読み出したために，同じ変数に対目の WRITE(turn, 0) の間に FENCE 命令を挿入する．

する未反映の WRITE である 2 行目の WRITE が赤くハイラ

スレッド T0 にも同様に FENCE 命令を挿入する．この

イトされている．

ように修正したモデルでモデル検査すると，エラーが報告されなかった．

4.4 議論
ピーターソンの相互排除の実験では，赤色のハイライト

4.3 並行 GC Staccato

表示が有用であった．最初の反例の中で WRITE が赤色に

Staccato は，ヒープ領域を FROM 空間と TO 空間の二ハイライトされた実行ステップは，上記の 2 回だけであつの部分空間に分けて管理するアルゴリズムである．コ

り，両方ともエラーに強く関連していた．修正後のモデル

レクタは FROM 空間からアプリケーションのスレッドの反例では，上記のステップ以降にもう 1 回 WRITE が赤色（ミューテータ）が参照可能なオブジェクトのみを TO 空にハイライトされる実行ステップがあったが，WRITE が赤間にコピーする．その間もミューテータはオブジェクトを色にハイライトされる実行ステップは十分に少なく，その使い続けるため，ミューテータが常に最新のオブジェクト

ほとんどがエラーに強く関連していたと言える．並行 GCにアクセスできるよう，適切な同期が必要になる．

Staccato でも，バグの原因となる WRITE は赤色のハイラ

Staccato は，プログラム順序と異なるメモリ順序で実行されることも想定しており，アルゴリズム中にフェンス命

イトで示されており，また，赤色のハイライトは 13 回と，ユーザが個々に確認できる程度の数であった．

令が使われている．しかし，Staccato にはミューテータの

しかし，ピーターソンの相互排除の実験の最初の反例で書いた値が TO 空間にコピーされないことがあるバグがあは，同じ実行ステップで変数 turn への WRITE も赤色でハることが指摘されている [4]．

イライトされていた．これは，デバッグの手順 (3) と (5)本実験では，Staccato のモデルを作ってバグを再現し，で修正した両方のエラーが混ざって表示されていたことに本反例可視化ソフトウェアを使ってその原因を理解した．

なる．また，Staccato の実験では，多くのバグに関係ない

以下では，本反例可視化ソフトウェアをどのように用いた未反映の WRITE があり，その一部は赤色でハイライトされかを述べる．

た．さらに複雑なアルゴリズムのデバッグする場合は，バSPIN が出力した最短の反例を本反例可視化ソフトウェ
アにロードして，ステップ実行の様子を確認した．この反グに関係ない未反映の WRITE が増えると考えられる．
これは，最短の反例として実行ステップ数のが最小の反8

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

例を使ったからである．WRITE を共有変数に反映させるとレッドが観測できる共有変数の値を読み解くことになる．

実行ステップ数が増えるので，結果としてエラーとは関係

しかし， MMLib は多数の内部的な変数を使っているので，ない WRITE も共有変数への反映が遅れる反例が選ばれた．

MMLib の内部構造を知っていても，目的の変数を探すの

MMLib を含む Promela モデル上での最短の反例ではなく，は手間がかかる．MMLib では各スレッドから観測できる

意味的に最も単純な反例を生成することができれば，より変数の値は，複数の内部的な変数の値に依存して決まるの

簡単にバグを理解できる．これは今後の課題である．

で，それを知るにはなおさら手間がかかる．

5. 既存の反例可視化ソフトウェアとの比較

5.3 フィルタリング機能

iSPIN[8] は SPIN 標準の反例可視化ソフトウェアである．

iSPIN では，図 9 の右上のボタンの左隣のテキストボッ

MMLib には特化していないが，ユーザが MMLib の内部

クスに正規表現を記述することで，表示する情報にフィル構造を理解していれば，iSPIN を使っても効率よくデバッ

タをかけることができる．例えば，一番上の「process ids」

グできるかどうか検討する．

というテキストボックスに「2」と記述すると，SPIN がプiSPIN はデバッグのために，反例の 1 文単位でステップ実行の様子を表示する．ただし，Never Claim を実行する

ロセスに割り振る ID の中に「2」を含むプロセスの実行のみが表示される．

文はステップとして扱わない．図 9 に，デバッグ用の GUI

この機能を用いて特定のプロセスの動きや，特定の共有を示す．GUI は，ステップ実行を制御する上段，モデル変数への WRITE が挿入されるキューに注目してログを見るとシーケンス図を表示する中段，反例と変数，チャネルをことができる．しかし，この機能を使っても，反例の中か表示する下段に分かれている．図 9 の中段左にはモデル

ら MMLib の内部状態に関する実行ステップや変数を隠蔽

がそのまま表示されており，ユーザはこのモデルと他の部

して，MMLib を使う Promela モデルの視点で必要な情報分に表示される情報との対応を取りながらデバッグする．

だけ得ることは難しい．

以下では，いくつかの観点で本反例可視化ソフトウェアと

iSPIN を比較する．

5.4 シーケンス図
図 9 の中段左にはシーケンス図が表示される．シーケン

5.1 反例の表示

ス図には，左から順に ID 順に スレッド が実行したチャ

図 9 の下段中央には反例の実行ステップが表示される．

ネルに対する操作が，ステップ実行の時系列に沿って表示

これは，SPIN が出力する反例がほとんどそのまま表示さされる．黄色の四角一つがチャネルに対する操作一つを表れる．例えば，表示されている 7 行目は，図 3 の 1 行目とす．例えば，一番上の四角はスレッド T1 が 11 番目のチャ同じである． 図 ??の反例の表示は図 3 の反例よりもシンネルに 1 を挿入したことを表している．赤色の破線は，現プルなように見えるが，これは図 ??の反例は SPIN に多く

在の実行ステップの位置を表している．

のオプションを与えて生成したからである． この表示は，

MMLib では，チャネルを用いて未反映の WRITE を保持

ステップ実行に連動して範囲が切り替わり，現在の実行ス

するキューを実装している．そのため，MMLib の実装を

テップの左端のステップ数が黄色でハイライトされる．し知っていれば，シーケンス図から WRITE がキューに挿入さかし，本研究の反例可視化ソフトウェアのようにモデル上れたり取り出されたりするタイミングを読み解くことがでに実行位置を視覚的に表示する機能はない．

きる．シーケンス図が，MMLib の内部実装ではなく，プロ

本研究の反例可視化ソフトウェアは，同時には反例中のグラムのモデル中に現れる変数名など名前を表示すれば，どれか一つの実行ステップしか表示されない．それに対し

本反例可視化ソフトウェアと相補的に組合わせて利用できて，iSPIN で反例がそのまま表示されるので，現在の実行ると考えられる．本反例可視化ソフトウェアにそのようなステップの前後の実行ステップも同時に見ることができる．

シーケンス図を表示する機能を追加することは今後の課題

これは MMLib を使っていないモデルでは便利である．しである．

かし，MMLib を使ったモデルでは，一つの共有変数アクセス命令の実行が多数の実行ステップに展開されるため，
共有変数アクセス命令が実行された周辺では前後の実行ス
テップが表示されてもあまり意味がない．

6. 関連研究
メモリモデルを考慮したモデル検査は盛んに行われているが，反例の理解を補助する仕組みは整備されていない．

Abe らは，McSPIN というメモリ順序を考慮してモデル
5.2 変数の値の表示

検査する手法を開発している [9]．McSPIN は，C 言語の反例中に表示される変数の一覧は下段左に，チャネルのコードを中間言語に変換した上で，メモリ順序を考慮した一覧は下段右に表示されている．これらの表示はステップ

Promela コードに変換し，SPIN によってモデル検査をす

実行と連動して切り替わる． ユーザは，この情報から各ス

る．変換後の Promela コードを SPIN でモデル検査する

92018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

図 9: iSPIN
Fig. 9 iSPINと，反例に相当するモデル検査の実行トレースが出力され網羅したオートマトンのグラフを表示し，その上で実行のる．しかし，出力されるのは中間言語の実行トレースであ様子を可視化する．プログラム順序の実行ではエラーが起るため，ユーザが作成する C 言語のコードと対応していな

こらないという前提で，メモリモデルを考慮したモデル検

い．そのため，ユーザが実行トレースを読み解いてデバッ

査を行う場合は，どんな実行パスを通ったかよりも，どのグを行うのは困難である．Travkin らも，WEAK2SC といタイミングでどのメモリアクセス命令がメモリに反映されうメモリ順序を考慮してモデル検査する手法を開発していたかの方がデバッグに重要である．そのため，本研究ではる [10], [11]．WEAK2SC では，C/C++のコードを LLVM

実際のモデルをそのまま表示し，その上にメモリ順序を可の IR コードを介して，メモリ順序を考慮した Promela モ

視化するという手法を採用した．

デルに変換しモデル検査する．変換後の Promela コード

反例に限らず，プログラムの実行の可視化の研究も行わ

は，goto 文で実行が制御される．そのため，反例と変換れている．Terada らは，プログラムのログから得た関数

前のモデルとの対応を取ってデバッグを行うのは困難であ呼び出しの情報を可視化してデバッグを支援する学生向け

る．これらに対して，本研究の反例可視化ソフトウェアは，

デバッグツール ETV を開発している [15]．ETV ではプロユーザが記述した Promela モデルの上でメモリ順序を表示

グラム上に情報を可視化する手法を採用している．丹野らする．そのため，反例を理解しやすい．

も，プログラム上に情報を可視化するデバッガを開発してメモリモデルを考慮したものでなければ，モデル検査

いる [16]．丹野らは，インタラクティブなプログラムのデの反例を可視化する研究は行われている．5 章で比較した

バッグのために，最近高い頻度で実行された行を視覚的に

iSPIN[8] は，SPIN 標準の反例可視化ソフトウェアである．

表示する．本研究でも Promela のモデル上に情報を可視化

Pakonen らは，ハードウェアのロジックをモデル検査すするが，本研究では，メモリ順序の情報を可視化した．

るためのツール MODCHK と，LTL 中の反例の理解に重Czyz らは，プログラムのログからクラスやメソッドの要な箇所を可視化するソフトウェアを開発している [12]．

呼び出しなどの関係を表すグラフや，実行のシーケンスグ

MODCHK では，反例のステップ実行をハードウェアのロラフを生成してデバッグを支援するデバッグツール JIVE

ジックを表すモデル上で可視化する．UPPAAL は，組みを開発している [17]．これは，大規模なプログラムの動作

込みシステムのモデリングやシミュレーション，モデル検を俯瞰して理解するためには有用である．本研究が対象と査を行う統合ツール環境である [13]．UPPAAL では，モするメモリモデルを考慮したデバッグでは，微視的な視点

デル検査の反例をシーケンスグラフやオートマトンのグラからモデルの動作を理解する方が重要であるため，本反例

フ上で可視化する．Aljazzar らは，モデル検査器 PRISM

可視化ソフトウェアでは Promela のモデル上で反例をスや MRMC の反例を可視化するツール DiPro を開発していテップ実行して表示することにした．

る [14]．DiPro では，モデル検査の際に，モデルの状態を10

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

7. おわりに[7]

メモリ順序を考慮したモデル検査をするためのライブラ
リ MMLib の反例可視化ソフトウェアを開発した．本反例[8]

可視化ソフトウェアは，反例に沿ってステップ実行する様子をモデル上に可視化する．本反例可視化ソフトウェアを使用することで，ユーザは MMLib の反例を読み解くこと[9]

なく，共有変数アクセス命令が共有変数に反映された順序などの情報を得ることができる．ケーススタディとして，
本反例可視化ソフトウェアを使い，プログラム順序とメモ[10]

リ順序が異なるようなメモリモデルで，ピーターソンの 相互排除 アルゴリズムで排他制御できるようにするための[11]

アルゴリズムの修正や，並行 GC Staccato のバグの理解を行った． このケースタディから，プログラム順序とは異なる順序で共有変数に反映された共有変数アクセス命令を，[12]

それが確定した実行ステップだけでハイライトするのが有用であることが分かった．

[13]

効率的なデバッグには単純な反例の生成が欠かせない．
これについて，現在の MMLib を用いたデバッグでは，SPINの最短の反例を出力する機能に頼っている．しかし，SPIN
は MMLib を展開したモデル上での最短の反例を生成し，[14]

それが必ずしも最も単純な反例とは限らない．特に，共有変数アクセス命令の反映順序は入れ替わる傾向にあり，本
反例可視化ソフトウェアでは多くの共有変数アクセス命令
がハイライトされるという問題がある．意味的に最も簡単

[15]
[16]

な反例を生成する仕組みを作り，この問題を解決するのが今後の課題である．
謝辞 本研究を行うにあたり，日本電信電話株式会社の丹野治門氏にさまざまなご教示を頂いたことを深く感謝致します．本研究の一部は，JSPS 科研費 16K00103 の助成[17]

115–116 (1981).
McCloskey, B., Bacon, D. F., Cheng, P. and Grove, D.:
Staccato: A Parallel and Concurrent Real-Time Compacting Garbage Collector for Multiprocessors, Research
Report RC24504, IBM (2008).
spinroot.com:
GettingStarted:Using
iSpin,
spinroot.com(online),availablefrom⟨http://spinroot.com/spin/Man/3 SpinGUI.html⟩(accessed 2018-12-14).
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).
Wehrheim, H. and Travkin, O.: TSO to SC via Symbolic
Execution, Proc. of HVC, LNCS, Vol. 9434, pp. 104–119(2015).
Travkin, O. and Wehrheim, H.: Verification of Concurrent Programs on Weak Memory Models, Proc. of ICTAC, LNCS, Vol. 9965, pp. 3–24 (2016).
Pakonen, A., Buzhinsky, I. and Vyatkin, V.: Counterexample Visualization and Explanation for Function Block
Diagrams, 2018 IEEE 16th International Conference on
Industrial Informatics (2018).
Behrmann, G., David, A., Guldstrand Larsen, K.,Håkansson, J., Pettersson, P., yi, W. and Hendriks,
M.: Uppaal 4.0, Third International Conference on the
Quantitative Evaluation of Systems, QEST 2006, pp.
125–126 (2006).
Aljazzar, H., Leitner-Fischer, F., Leue, S. and Simeonov,
D.: DiPro : A Tool for Probabilistic Counterexample
Generation, Model Checking Software, LNCS, Springer
Berlin Heidelberg, pp. 183–187 (2011).
Terada, M.: ETV: A Program Trace Player for Students,
SIGCSE Bull., Vol. 37, No. 3, pp. 118–122 (2005).
丹野治門，岩崎英哉： プログラムを停止させないデバッグを可能とする手法の提案，日本ソフトウェア科学会第35 回大会講演論文集 (2018).
Czyz, J. K. and Jayaraman, B.: Declarative and VisualDebugging in Eclipse, Proceedings of the 2007 OOPSLA
Workshop on Eclipse Technology eXchange, eclipse ’07,
ACM, pp. 31–35 (2007).

を受けたものです．
参考文献
[1]

[2]

[3]
[4]

[5]

[6]

松元稿如，鵜川始陽，安部達也： メモリモデルを考慮したメモリアクセス命令を提供する SPIN 用ライブラリ，ソフトウェア工学の基礎，Vol. 23, pp. 63–72 (2016).
Matsumoto, K., Ugawa, T. and Abe, T.: Improvementof a Library for Model Checking under Weakly Ordered
Memory Model with SPIN, Journal of Information Processing, Vol. 26, pp. 314–326 (2018).
Holzmann, G. J.: The SPIN Model Checker, AddisonWesley (2003).
Ugawa, T., Abe, T. and Maeda, T.: Model Checking
Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models, Proc. ACM Program.
Lang., Vol. 1, No. OOPSLA, pp. 53:1–53:26 (2017).
Iiboshi, H. and Ugawa, T.: Towards Model Checking
Library for Persistent Data Structures, 2018 IEEE 7th
Non-Volatile Memory Systems and Applications Symposium (NVMSA), pp. 119–120 (2018).
Peterson, G. L.: Myths about the mutual exclusion problem, Information Processing Letters, Vol. 12, No. 3, pp.

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

Society Japan Chapter FOSE Young
Researcher Award 受賞．

11

2018-4-(8): 情報処理学会プログラミング研究会 2019 年 1 月 18 日

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

12