はじめに

単純ですが具体的な例を示したいと思います。今回題材とするのは、「クリティカルセクション問題」です。これは並行処理のプログラムが資源を共有したりする場合に出くわす問題です。

今回、検証に使うツールはモデル検査ツールPAT(Process Analysis Toolkit)とします。利用の際にところどころツールの画面などができますが、ツールそのものの使い方の詳細は省かせていただきます。もちろん、同等の機能を持つ別なツールを使っても同様の検証が可能です。

クリティカルセクション問題

この問題は並行動作する２つのスレッドに対して、以下の要求が満たされているアルゴリズムを構成することです。

要求1 : 排他制御。あるスレッドがクリティカルセクションを実行中は他のスレッドのクリティカルセクションを実行する事はできない。
要求2 : あるスレッドがクリティカルセクション以外の処理を実行している場合には他のスレッドはいつでもそのクリティカルセクションを実行できる。

この２つの要求を満たすアルゴリズムはすでにいくつか知られているものがあります(Dekker's Algorithmなど）。しかし、本記事では、そのような完成したプログラムではなく、道半ばで上記の要求を満たしていないGo言語のプログラムを示し、それを形式言語であるCSPで記述し、検証する方法を説明します。

なお、今回の検証は要求1に絞って説明する事にします。

コード例：要求1がNG - 同時に2つのThreadのクリティカルセクションが動作可能になってしまう

go言語での記述

各スレッドの定義（コード片）を載せます。

var Thread0inside int = 0;
var Thread1inside int = 0;

func ThreadZero() {
  for {
    for Thread1inside == 1 {}
    Thread0inside = 1;
    CriticalSectionZero()
    Thread0inside = 0;
    OtherStuffZero();
  }
}

func ThreadOne() {
  for {
    for Thread0inside == 1 {}
    Thread1inside = 1;
    CriticalSectionOne()
    Thread1inside = 0;
    OtherStuffOne();
  }
}

それぞれのスレッドは、まず、相手のスレッドがクリティカルセクションに入っているかどうかを確認します。入っていないないならクリティカルセクションに入りますが入っている間はそこにとどまります（ロック）。クリティカルセクションに入っているかどうかはそれぞれのスレッドが持つフラグの値を確認します。
と、一見、特に問題はなさそうですが・・

動かして確認したい人のために

また、当然ながらここに示したコード片だけでは、実行して確認する事はできません。このプログラムを確認するには以下の追加コードが必要になります：

各スレッドの「無限ループ」を有限にする
定義されていない関数を定義する
- CriticalSectionZero(),CriticalSectionOne(),OtherStuffZero(),OtherStuffOne()はここを実行している事わかるような表示を行うようなものにする(fmt.Printfを使うなど)。
main関数を作る
- mainの中でThreadZero()とThreadOne()をgo routineとして起動
- ２つのThreadが終了するのに十分なWaitを行う(time.Sleepなどを利用)

goのコード(参考程度にどうぞ)

https://gist.github.com/fujim2/dc3625b8f20fc5eb40c3fb91e3d15356
critical_bad.go の各スレッドのsleepをコメントアウトすると２つのスレッドのクリティカルセクションが重なって実行されるのが観測できます。

CSPでの記述と検証

上記プログラムをCSPで記述してみます。

var Thread0inside  = 0;
var Thread1inside  = 0;

ThreadZero() = 
    [!(Thread1inside == 1)]
    T0Start
    ->CriticalSectionZero{Thread0inside = 1}
    ->T0End{Thread0inside = 0}
    ->OtherStuffZero
    ->ThreadZero();

ThreadOne() = 
  [!(Thread0inside == 1)]
   T1Start
    ->CriticalSectionOne{Thread1inside = 1}
    ->T1End{Thread1inside = 0}
    ->OtherStuffOne
    ->ThreadOne();

System = ThreadZero() || ThreadOne();

プログラミング言語に対応するCSPでの表現にはいくつかバリエーションがあるのですが、今回はできるだけコードと対応が付くようなものにしてみました。

状態の遷移空間を確認してみる

多くの「モデル検査ツール」は、「検査」の機能だけでなく、シミュレーションの機能を持っている事が多いです。ここでは、PATのシミュレーション機能を使って、このプログラムの振る舞いの空間を可視化してみます。

なかなか複雑ですね。この中のどこかに問題（要件を満たさない状況）があったとしても、なかなか見つけるのは大変かもしれません。

検証

さて、モデル検査ツールの本領を発揮してもらいましょう。以下の様なPATの検証式を使って検証します。今回は、モデル検査でよく使われる「時相論理式(temporal logic)」を使った検証は行わず、ツールの方ですでに用意されているものを使います。

検証式

以下の様な検証式を使って検証したいと思います。


#assert System deadlockfree;
#define badstatus (Thread0inside==1 && Thread1inside == 1);
#assert System reaches badstatus;

1行目はそもそも、Systemがデッドロックしないという検証式です。
2行目は２つのスレッドが同時にクリティカルセクションに入っているという「bad status」の定義です
3行目はSystemがこのbadstatusという状態に到達する可能性がある、という検証式です。

２つの検証式はの結果を確認してみます。PATでは、検証のための画面で検証式を選択し、「verify」というボタンを押すことで検証が開始し、結果はコンソールに表示されます。結果、

１つ目の検証式はVALIDでした。つまり「デッドロックしない」事が検証できました。
２つ目の検証式もVALIDでした。つまり、badstatusになるという事ですから問題がある、という指摘です。

２つ目の検証式は「到達可能性(reachability)」を検査したのですが、ツールは、検査結果を確認した後に、「Simulate Witness Trace」というボタンを押すことで、シミュレーション機能と連動して、パスを表示してくれます(検証の機能とシミュレーションの機能が連動しています）。

左側の表示エリアにはステップ毎の変数の値などが表示されていますが、Thread1insideとThread0insideの値がともに１になっている事(クリティカルセクションが同時に実行されている）がわかります。

CSPのコード(参考程度にどうぞ)

なお、このプログラムの問題が、これだけかどうかはこの時点ではわかりません。

さいごに

ここで示したプログラムコードは非常に小さいものですが、それでも、思ったようにはつくれない、それが「並行・並列」プログラミングの難しさです。そして、その原因の多くは並行に動作するために起こる動作タイミングの非決定性、そしれそれに関係して肥大している振る舞い空間にあると思います。このおかげで、往々にしてプログラムは直観に反する振る舞いの経路をたどって、思いもよらない不具合を引き起こします。

なお、本記事の題材は、「並列コンピューティング技法 - 実践マルチコア/マルチスレッドプログラミング(Clay Breshears著)」訳本の第３章「正当性の検証と性能測定」の例を参考にしました（コード・文書ともにコピペなどはしておりません）。

今回は以上です。では。

golangの並行処理のための言語要素に対応するCSPの記述を理解して形式検証の実践を開始しよう(検証編：クリティカルセクション）