Think Stitch
  最近の更新


Pthread Model Checker の紹介

Pthread プログラム用のモデル検査ツールを開発したので紹介したいと思います.名前は Pthread Model Checker といいます.

「モデル検査」という名前をはじめて聞いたという人のために少し前置きをします.ご存じの方は2まで飛ばしてください.

0  マルチスレッドプログラミングは難しい

よくマルチスレッドプログラミングは難しいといわれます.難しい理由として挙げられるものには次のものがあります:

デッドロックはご存知だと思います.すべてのスレッドが待ち状態に入って動かなくなってしまう現象です.これに対してライブロックという名前はあまりメジャーではないかもしれません.これは,いくつかのスレッドが動作しているのに,みな進捗のない動作を繰り返しているだけでシステム全体としては機能しなくてなってしまう現象です.よく見かけるのは,CPU の使用率が 100 % になっていて,マウスカーソルが砂時計になったまま何も反応しなくなるあの現象です.

同じ状況を設定しているつもりなのに,問題が発生したりしなかったりする性質は非決定性と呼ばれています.これは各スレッドが実行される順序が不定であることから起こる現象です.1度テストにパスしたからといって動作が保証できるわけではないという点が非決定性のやっかいなところです.

最後の問題は状態数爆発(状態爆発)と呼ばれています.おおざっぱな見積もりをすると,システムを構成するコンポーネントの数が増えると,システム全体としての状態は掛け算で増えていきますから,コンポーネントの数に対して指数関数的に状態数が増えていきます.したがって,人間が手作業のテストで網羅できる範囲はすぐに超えてしまいます.

こんなわけでマルチスレッドプログラミングは難しいわけです.

1  モデル検査とは

マルチスレッドプログラミングの難しさを克服する方法の1つとして有効なのがモデル検査です.モデル検査というのは,プログラムの主要な振る舞いを抽象的なモデルとして記述し,それが持つすべての状態と実行パスをコンピュータのパワーを使って網羅的に調べ上げるという手法です.抽象的なモデルというのは,コードを考え始めるときにはじめに書く全体構造のスケルトン,あるいはアルゴリズムを記述するときの擬似コードのようなものです.

この方法ならばタイミングの違いなどによる非決定性も含めてすべて調べ上げることができるので,テストで再現できない問題も確実に捉えることができます.さらにコンピュータで調べ上げますから,人間がテストするのに比べて5桁も6桁も多い状態数,つまり1,000万とか1億といった数の状態を調べることができます.

このようにパワフルなモデル検査なのですが,残念ながらいくつか欠点もあります.

前者の限界はなかなか悩ましいのです.時間を投資してモデル検査に挑戦してみたけれど,結局状態爆発で成果を得られなかったというリスクがあるからです.それでも役に立つ場合はたくさんあります.モデル検査は道具なので,使えるところでかしこく使うというのがよいと思います.

世にモデル検査ツールはいろいろあるのですが,それらの間で仕様記述の方法としてよく使われているのは時相論理という論理の1種です.残念ながらこれは理解して使いこなすのがやや難しいようです.他にも仕様として状態遷移モデルを渡すようなものもあります.いずれの場合もちょっと敷居が高いのは,プログラミング言語の他にモデル検査専用の仕様記述言語を勉強しなければならないという点です.勉強のコストもそうですが,検査が終わったあと,そのモデルを再度プログラミング言語で書き直さなければならないという点も問題です.1つは書き直しのコストがかかること,もう1つは書き直しのときに性質を壊してしまったり,別の問題を入れ込んでしまったりする危険性があることです.

2  Pthread Model Checker の特徴

状態爆発の問題を解決することはかんたんにはいかないので,主にモデルの記述や仕様の記述の問題を解決しようと思って今回開発したのが Pthread Model Checker です.

Pthread Model Checker の特徴は次のとおりです:

3  Pthread Model Checker の実行例

さっそく Pthread Model Checker を使ってみることにします.まずはかんたんなところからはじめます.最初の例は,整数型のグローバル変数 count を1つ用意し,それからスレッドを2つ起動します.各スレッドはそれぞれ独立に count をインクリメントします.スレッドが終了したあと count が 2 になっていることを assert で確認してみましょう.

3.0  モデル

モデル全体は次のようになります.ご覧のとおり pthread を使ったふつうのC言語のコードです.ヘッダファイルの include は,このコードをこのままコンパイルして実行できるように入れてあります.モデル検査のためだけであれば不要です. Pthread Model Checker は #include ディレクティブを無視します.

C言語サブセットの細かい仕様に深入りすると話の流れがわかりにくくなるので,注意する点が出てきたときに解説することにします.詳細な仕様についてはリファレンスマニュアルを参照してください.

increment.c

#include <stdio.h>
#include <stdbool.h>
#include <stdint.h>
#include <pthread.h>
#include <assert.h>

pthread_t pth1, pth2;
int count;

void *thread(void *arg)
{
    count++;
    return NULL;
}

int main(void)
{
    void *r;
    pthread_create(&pth1, NULL, &thread, NULL);
    pthread_create(&pth2, NULL, &thread, NULL);
    pthread_join(pth1, &r);
    pthread_join(pth2, &r);
    assert(count == 2);
    return 0;
}

3.1  検査プログラムの生成

このモデルを Pthread Model Checker で検査するには,まず ptmc コマンドにかけます. Pthread Model Checker は,検査を高速に実行するために,Pthread Model Checker 自身がモデルを解釈実行検査するのではなく,一度別のC言語のソースコードに変換します.このソースコード自身が検査を実行するプログラムになります.これをコンパイラでコンパイルすると,実際に検査を行う実行バイナリができるわけです.このモデル・ソースコード変換を行うコマンドが ptmc です.

ptmc コマンドの書式は次のとおりです:

ptmc model check-src

実際に上のモデル increment.c を変換してみます.出力ファイルは increment.ptmc.c としました.

$ ptmc increment.c increment.ptmc.c

実は ptmc コマンドを実行すると,検査実行プログラムのソースコードの他にもう1つ,状態遷移図のファイルが生成されます. Pthread Model Checker は与えられたモデルを状態遷移モデルに変換して検査をするのです.ptmc コマンドは,この状態遷移モデルを図(グラフ)として出力してくれます.これは後でレポートを見ながら問題を分析するときに役に立ちます.

状態遷移図は Graphviz の dot 形式で出力されます.これを Graphviz の dot コマンドで PNG や PDF に変換すれば閲覧することができます.ここでは PNG に変換してみます.

$ dot -T png -o increment.png increment.c.dot

するとこのような状態遷移図が得られます:

左の長いパスが main 関数の流れ,右の短い方が thread 関数の流れです.

右の流れを少し詳細に見てみると,count のインクリメント count++load-scalarstore-scalar の2つの遷移に分解されていることがわかるでしょうか.遷移の矢印についているラベル,例えば (load-scalar t5 count):12 とある部分です.これはグローバル変数 count の値を,内部的に自動生成された一時変数 t5 に読み込んでいるという意味です.後ろの 12 という数はモデルの行番号で,count++ の行です.store-scalar の遷移にも 12 とありますから,1つの行から2つの遷移ができています.

実際 CPU はインクリメントをこのように読み書き2動作で行うわけです.そしてマルチスレッドの場合,2つの動作の間で別のスレッドが動く可能性があり,これが話をややこしくするわけです.

Pthread Model Checker はこのようにモデルのコードを基本動作に分解し,すべての可能な組み合わせを調べ上げるのです.

話を戻して検査を実行しましょう. ptmc コマンドで変換された検査実行プログラムのソースコードを gcc でコンパイルします.このとき Pthread Model Checker のライブラリをリンクします.検査を並列に行うために,Pthread Model Checker 自身も pthread を使っているので,pthread ライブラリもリンクします.

$ gcc -o increment increment.ptmc.c -L libpath -lptmc -pthread

これで検査実行プログラムの実行ファイルができました.実行してみるとすぐに次のようなメッセージが表示されます:

$ ./increment
assertion violation
increment.c:23: assert(count == 2);

これは assert 違反を発見したことを示します.このとき違反についての詳細な情報がレポートファイル increment.c.report に出力されています.中身はこんな感じです.先頭には検査のパラメータ値等があって,その後に長いログのようなものがあります.これは初期状態から assert 違反があった状態までのパスです.Pthread Model Checker は違反状態を見つけるだけでなく,初期状態からその状態までの最短パスを見つけて提示してくれます.

version: 1.0.0
model_filename: "increment.c"
num_workers: 1
heap_size: 1073741824 bytes
hashtable_size: 4000037 entries
assertion violation
increment.c:23: assert(count == 2);
num-of-states: 40

#0 main nil
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 1
------------------------
#1 main create pth1
19: pthread_create(&pth1, NULL, &thread, NULL);
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 2
1 pth1 8
    arg = 0
------------------------
#2 main create pth2
20: pthread_create(&pth2, NULL, &thread, NULL);
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 8
    arg = 0
2 pth2 8
    arg = 0
------------------------
#3 pth2 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 8
    arg = 0
2 pth2 9
    t5 = 0
------------------------
#4 pth1 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 9
    t5 = 0
2 pth2 9
    t5 = 0
------------------------
#5 pth1 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 10
2 pth2 9
    t5 = 0
------------------------
#6 pth1 exit
13: return NULL;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 0
    retval = 0
2 pth2 9
    t5 = 0
------------------------
#7 pth2 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 0
    retval = 0
2 pth2 10
------------------------
#8 main join pth1
21: pthread_join(pth1, &r);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 4
1 pth1 ---
2 pth2 10
------------------------
#9 pth2 exit
13: return NULL;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 4
1 pth1 ---
2 pth2 0
    retval = 0
------------------------
#10 main join pth2
22: pthread_join(pth2, &r);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 5
------------------------
#11 main load count
23: assert(count == 2);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 6
    t6 = 1
------------------------

各要素を解説しましょう.まず # で始まる2行からなる部分は遷移を表しています:

------------------------
#1 main create pth1
19: pthread_create(&pth1, NULL, &thread, NULL);
------------------------

# のあとの数は,この遷移が初期状態から何ステップ目の遷移であるかを示しています.つづく main はこの遷移を行ったのが main スレッドであるという意味です.行った動作は create で,これはスレッドの生成を意味します.pth1 はモデルで定義した pthread_t 型の変数名で,これが生成されたスレッドを示します.次の行はこの遷移に対応するモデルのソースコード行です.

次の部分へ行きます.下に切り出した比較的長めのブロックは状態を表しています.レポートのパスでは先程の遷移とこの状態が交互に現れます.

はじめにグローバル変数の値が表示されています.この例では count は 0 です.つづいてミューテックスの状態が表示されるのですが,このモデルではミューテックスを使っていないので空です.

つづいて各スレッドの状態が表示されます.先頭の数は Pthread Model Checker がつけたスレッド番号です.次にスレッドの名前があって,さらに数があります.これはスレッドがいる状態番号で,先に見た状態遷移図のノードの番号です.この例だと main スレッドは状態 3 にいます.状態遷移図を見ると,create 遷移をしたあとの状態であることがわかります.

もう1つ,スレッド pth1 があります.これは生成直後の状態 8 にいます.スレッドがローカル変数を持っている場合は,インデントされて表示されます.

------------------------
global vars:
    count = 0
mutex:
thread:
0 main 2
1 pth1 8
    arg = 0
------------------------

最初なのでもう少し丁寧に見てみましょう.4ステップ目の部分です.ここではスレッド pth1 が count の値を load し,それから +1 した値を store しています.結果として count は 1 になりました.

------------------------
#4 pth1 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 9
    t5 = 0
2 pth2 9
    t5 = 0
------------------------
#5 pth1 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 10
2 pth2 9
    t5 = 0
------------------------

さて,パスの見方がだいたいわかったところで,問題の分析に移りましょう.問題はなぜ assert 違反が起こったのかということです.

遷移の部分だけを取り出してみると次のようになります:

#0 main nil
#1 main create pth1
#2 main create pth2
#3 pth2 load count
#4 pth1 load count
#5 pth1 store count
#6 pth1 exit
#7 pth2 store count
#8 main join pth1
#9 pth2 exit
#10 main join pth2
#11 main load count

これを見ると,スレッド pth2 の #3 load と #7 store の間に,スレッド pth1 の #4 load と #5 store が挟まれていることがわかります.すでに知っているとは思いますが,このせいで count は 2 にならないのですね.どちらのスレッドも初期値 0 を読んで,1 を書いているだけだからです.

スレッドの動作が混じり合わなければ問題は起こりません.混じり合う組み合わせがたくさんあって,そのうちのいくつかで問題が起こります.どの組み合わせが起こるかはわかりません.これが非決定性のでどころです. Pthread Model Checker はすべての組み合わせを検査して問題を発見するわけです.

このモデルを実行してみても,まず問題は起こらないでしょう.インクリメントにかかる時間はわずかなので,2個めのスレッドを起動している間に1個めのスレッドはインクリメントを完了してしまうからです.

しかしこれが実コードの中にあって,スレッド開始のタイミングがほとんどそろうようなケースがあったら危険です.再現性の低いやっかいな問題となります.

3.2  ミューテックスによる排他処理

この問題を解決するにはミューテックスを用意して排他処理をします.

increment2.c

#include <stdio.h>
#include <stdbool.h>
#include <stdint.h>
#include <pthread.h>
#include <assert.h>

pthread_t pth1, pth2;
pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
int count;

void *thread(void *arg)
{
    pthread_mutex_lock(&m);
    count++;
    pthread_mutex_unlock(&m);
    return NULL;
}

int main(void)
{
    void *r;
    pthread_create(&pth1, NULL, &thread, NULL);
    pthread_create(&pth2, NULL, &thread, NULL);
    pthread_join(pth1, &r);
    pthread_join(pth2, &r);
    assert(count == 2);
    return 0;
}

変数 count のインクリメントを lock と unlock ではさみました.コンパイルをして検査をしてみると,問題が解決できたことを確認できます.(問題がないときは寡黙です :P)

$ ptmc increment2.c increment2.ptmc.c
$ gcc -o increment2 increment2.ptmc.c -L libpath -lptmc -pthread
$ ./increment2
$

4  まとめ

Pthread Model Checker を紹介しました.

マルチスレッドプログラミングは難しいですけれども,モデル検査ツールを使えばコードの正しさに確信を持てるようになります.再現しにくい問題も確実に発見できるからです.ツールのレポートは問題の分析と解決に大きな助けとなります.

Pthread Model Checker はC言語でモデルを書くことができるので,すぐに使いはじめることができます.調べたい性質も assert を書くだけなのでかんたんです.

次はデッドロック検査の例を紹介します.

2017/10/08

© 2013-2017 PRINCIPIA Limited