Think Stitch
  最近の更新


Pthread Model Checker によるバリアの安全性検査

Pthread Model Checker の紹介その3です.

今回は Pthread Model Checker の機能の1つであるグローバル assert を使って,バリアの安全性を検査してみたいと思います.

0  バリア

バリア (barrier) というのは複数のスレッドが同時に同期する機構のことです.ランデブ (rendezvous) ともいわれます.それぞれ自分の処理をしていたスレッドが,一度一か所に全員集合して,それからまた個々の処理を再開する,この全員集合がバリアです.

POSIX thread (pthread) にはバリア専用の関数があります. pthread_barrier_wait です.これが使えるときには使えばいちばん確実です.

しかし全員集合するときは,その待合室に来たときに何か仕事をしたいということがよくあります.特に自分がいちばん遅れてきたかどうか判定したいことはよくあります.ただ,これは pthread_barrier_wait でも識別できます.それ以外にもロックついでにちょっとデータ構造をいじりたいとかそういうことがあります.

そういうときは手持ちのプリミティブな武器であるミューテックスと条件変数を組み合わせて作ることになります.このようなときにはじめにすべきことは,すでに同じことをしている人がいないかどうか調べることです.もし望む解が教科書に載っていたり,同じ解がたくさん使われているようならばそれを使えば安心でしょう(たぶん).

しかし検索しても見つからない場合は自分で考えるしかありません.そうするととたんに不安になります.マルチスレッドのアルゴリズムはなかなか期待通りに動いてくれないからです.

前置きが長くなりましたが,そこでモデル検査をしようという話です.

1  バリアのモデル

バリアの考え方はこうです: 待合室に到着したスレッドの数を数えて,全員揃うまで条件変数で待ちます.最後のスレッドは自分が最後であることを認識して,全員を起こします.

スレッドを数えるためにカウンタ count が必要です.これを複数のスレッドで共有しますから排他制御のためにミューテックスが必要です.そして待ち合わせのために条件変数を用意します.

#define N 4

pthread_t pth[N];
pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
pthread_cond_t cv = PTHREAD_COND_INITIALIZER;
int count;

void barrier(void)
{
    pthread_mutex_lock(&m);
    count++;
    if (count == N) {
        pthread_cond_broadcast(&cv);
    } else {
        while (count < N) {
            pthread_cond_wait(&cv, &m);
        }
    }
    pthread_mutex_unlock(&m);
}

void *thread(void *arg)
{
    // A
    barrier();
    // B
    return NULL;
}

int main(void)
{
    for (int i = 0; i < N; ++i) {
        pthread_create(&pth[i], NULL, &thread, NULL);
    }
    for (int i = 0; i < N; ++i) {
        pthread_join(pth[i], NULL);
    }
    return 0;
}

まずミューテックスをロックして count をインクリメントします.もし最後の到着者でなければ条件変数の待ちに入ります.最後の到着者は pthread_cond_broadcast で全員を起こします.

2  安全性の検査

問題はこのバリアが期待通りに機能することをどのように調べたらいいかということです.

関数 barrier の呼び出し部分で全員が一度集合するということは,A の部分の処理と B の部分の処理が混じり合うことはないということです.文字通りバリアで仕切られているわけですから.

そこでこう考えます.2つの変数 a, b を用意します.どちらも初期値は 0 です. A の部分では a をインクリメントします.B の部分では b をインクリメントします.すると2つの処理は混じり合わないわけですから b が 0 でなければ a は必ず N であるはずです.つまり全員がバリアを通過したから,b がインクリメントされたということです.

これを条件式で書くと b == 0 || a == N となります.

3  グローバル assert

次の問題は,この条件をどこで検査するかということです.この例ではおそらく A, B それぞれのインクリメントの前後,合計4箇所に assert を入れれば十分しょう(たぶん).しかしできればプログラムの実行全体を通して条件が成り立つことを調べたいでしょう.そもそも同じ assert をあちこちにばらまきたくないですしね.

Pthread Model Checker はこの目的のためにグローバル assert という機能を持っています.ふつうの assert と違って,プログラムの実行全体を通して常に条件を監視してくれる assert です.

グローバル assert は1行コメントの中に次のフォーマットで書きます:

// @ASSERT(expression)

これだけで常に条件式 expression を監視してくれます.もし違反する状態があれば,ふつうの assert やデッドロックのようにパスをレポートしてくれます.

4  安全性検査のモデル

変数 a, b と,それらの排他制御用のミューテックス m2 を用意して安全性検査のモデルにします.グローバル assert はどこに書いてもいいのですが,変数 a, b のそばがいいですよね.

#define N 4

pthread_t pth[N];
pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
pthread_cond_t cv = PTHREAD_COND_INITIALIZER;
int count;
int a;
int b;

// @ASSERT(b == 0 || a == N)

void barrier(void)
{
    pthread_mutex_lock(&m);
    count++;
    if (count == N) {
        count = 0;
        pthread_cond_broadcast(&cv);
    } else {
        while (count < N) {
            pthread_cond_wait(&cv, &m);
        }
    }
    pthread_mutex_unlock(&m);
}

void *thread(void *arg)
{
    pthread_mutex_lock(&m2);
    a++;
    pthread_mutex_unlock(&m2);

    barrier();

    pthread_mutex_lock(&m2);
    b++;
    pthread_mutex_unlock(&m2);

    return NULL;
}

int main(void)
{
    for (int i = 0; i < N; ++i) {
        pthread_create(&pth[i], NULL, &thread, NULL);
    }
    for (int i = 0; i < N; ++i) {
        pthread_join(pth[i], NULL);
    }
    return 0;
}

検査してみると問題がないことがわかります.

5  モデルを壊してみる

最初は,ほんとうにグローバル assert が機能しているのか不安でしょうから,ちょっと条件を変えてみましょう.

// @ASSERT(!(b == 1 && a == N))

b == 1 && a == N というのは全員が揃ったあと一人だけがインクリメントをした状態(の中のどれか1つ)です.それに否定がついていますから「そんな状態はない」という意味になります.これを常に監視するわけですから,もし違反があったら,それは「そういう状態がある」ということになります.

このようにグローバル assert による検査は「〜という状態はあるか?」という問い合わせだと考えることができます.問い合わせしたい条件の否定をグローバル assert に指定すればいいわけです.

実際に検査を行うと違反が見つかります.レポートの最後を見ると,確かに a == 4 && b == 1 (N=4) の状態があることがたしかめられました.

version: 1.0.0
model_filename: "barrier1.c"
num_workers: 1
heap_size: 1073741824 bytes
hashtable_size: 4000037 entries
spurious_wakeups: off
global assertion violation
barrier1.c:17: // @ASSERT(!(b == 1 && a == N))
num-of-states: 19680
time: 50 ms
heap: 1182680 bytes

#0 main nil
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 1
------------------------
#1 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 2
    i = 0
------------------------
#2 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 3
    i = 0
------------------------
#3 main create pth[0]
51: pthread_create(&pth[i], NULL, &thread, NULL);
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 10
    arg = 0
------------------------
#4 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 2
    i = 1
1 pth[0] 10
    arg = 0
------------------------
#5 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 3
    i = 1
1 pth[0] 10
    arg = 0
------------------------
#6 main create pth[1]
51: pthread_create(&pth[i], NULL, &thread, NULL);
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 1
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
------------------------
#7 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 2
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
------------------------
#8 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 3
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
------------------------
#9 main create pth[2]
51: pthread_create(&pth[i], NULL, &thread, NULL);
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 10
    arg = 0
------------------------
#10 pth[2] lock m2
35: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 pth[2]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 11
------------------------
#11 pth[2] load a
36: a++;
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 pth[2]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 12
    t10 = 0
------------------------
#12 pth[2] store a
36: a++;
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 pth[2]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 13
------------------------
#13 pth[2] unlock m2
37: pthread_mutex_unlock(&m2);
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 14
------------------------
#14 pth[2] lock m
21: pthread_mutex_lock(&m);
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 15
------------------------
#15 pth[2] load count
22: count++;
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 16
    t14 = 0
------------------------
#16 pth[2] store count
22: count++;
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 17
------------------------
#17 pth[2] load count
23: if (count == N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 18
    t15 = 1
------------------------
#18 pth[2] tau
23: if (count == N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 21
------------------------
#19 pth[2] load count
26: while (count < N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 10
    arg = 0
3 pth[2] 22
    t16 = 1
------------------------
#20 pth[1] lock m2
35: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 11
3 pth[2] 22
    t16 = 1
------------------------
#21 pth[1] load a
36: a++;
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 12
    t10 = 1
3 pth[2] 22
    t16 = 1
------------------------
#22 pth[2] tau
26: while (count < N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[2]
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 12
    t10 = 1
3 pth[2] 23
------------------------
#23 pth[1] store a
36: a++;
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m pth[2]
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 13
3 pth[2] 23
------------------------
#24 pth[2] wait cv m
27: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m <unlocked>
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 13
3 pth[2] 24 wait cv
------------------------
#25 pth[1] unlock m2
37: pthread_mutex_unlock(&m2);
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 14
3 pth[2] 24 wait cv
------------------------
#26 pth[1] lock m
21: pthread_mutex_lock(&m);
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 15
3 pth[2] 24 wait cv
------------------------
#27 pth[1] load count
22: count++;
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 16
    t14 = 1
3 pth[2] 24 wait cv
------------------------
#28 pth[1] store count
22: count++;
------------------------
global vars:
    count = 2
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 17
3 pth[2] 24 wait cv
------------------------
#29 pth[1] load count
23: if (count == N) {
------------------------
global vars:
    count = 2
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 18
    t15 = 2
3 pth[2] 24 wait cv
------------------------
#30 pth[0] lock m2
35: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 2
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 pth[0]
thread:
0 main 5
    i = 2
1 pth[0] 11
2 pth[1] 18
    t15 = 2
3 pth[2] 24 wait cv
------------------------
#31 pth[0] load a
36: a++;
------------------------
global vars:
    count = 2
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 pth[0]
thread:
0 main 5
    i = 2
1 pth[0] 12
    t10 = 2
2 pth[1] 18
    t15 = 2
3 pth[2] 24 wait cv
------------------------
#32 pth[1] tau
23: if (count == N) {
------------------------
global vars:
    count = 2
    a = 2
    b = 0
mutex:
    m pth[1]
    m2 pth[0]
thread:
0 main 5
    i = 2
1 pth[0] 12
    t10 = 2
2 pth[1] 21
3 pth[2] 24 wait cv
------------------------
#33 pth[0] store a
36: a++;
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[1]
    m2 pth[0]
thread:
0 main 5
    i = 2
1 pth[0] 13
2 pth[1] 21
3 pth[2] 24 wait cv
------------------------
#34 pth[1] load count
26: while (count < N) {
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[1]
    m2 pth[0]
thread:
0 main 5
    i = 2
1 pth[0] 13
2 pth[1] 22
    t16 = 2
3 pth[2] 24 wait cv
------------------------
#35 pth[0] unlock m2
37: pthread_mutex_unlock(&m2);
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 14
2 pth[1] 22
    t16 = 2
3 pth[2] 24 wait cv
------------------------
#36 pth[1] tau
26: while (count < N) {
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[1]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 14
2 pth[1] 23
3 pth[2] 24 wait cv
------------------------
#37 pth[1] wait cv m
27: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 14
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#38 pth[0] lock m
21: pthread_mutex_lock(&m);
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 15
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#39 pth[0] load count
22: count++;
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 2
1 pth[0] 16
    t14 = 2
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#40 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 2
    i = 3
1 pth[0] 16
    t14 = 2
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#41 main tau
50: for (int i = 0; i < N; ++i) {
------------------------
global vars:
    count = 2
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 3
    i = 3
1 pth[0] 16
    t14 = 2
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#42 pth[0] store count
22: count++;
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 3
    i = 3
1 pth[0] 17
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
------------------------
#43 main create pth[3]
51: pthread_create(&pth[i], NULL, &thread, NULL);
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 17
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 10
    arg = 0
------------------------
#44 pth[0] load count
23: if (count == N) {
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 18
    t15 = 3
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 10
    arg = 0
------------------------
#45 pth[3] lock m2
35: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 18
    t15 = 3
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 11
------------------------
#46 pth[0] tau
23: if (count == N) {
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 21
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 11
------------------------
#47 pth[3] load a
36: a++;
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 21
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 12
    t10 = 3
------------------------
#48 pth[0] load count
26: while (count < N) {
------------------------
global vars:
    count = 3
    a = 3
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 22
    t16 = 3
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 12
    t10 = 3
------------------------
#49 pth[3] store a
36: a++;
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 22
    t16 = 3
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 13
------------------------
#50 pth[0] tau
26: while (count < N) {
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m pth[0]
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 23
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 13
------------------------
#51 pth[3] unlock m2
37: pthread_mutex_unlock(&m2);
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 23
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 14
------------------------
#52 pth[0] wait cv m
27: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 14
------------------------
#53 pth[3] lock m
21: pthread_mutex_lock(&m);
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 15
------------------------
#54 pth[3] load count
22: count++;
------------------------
global vars:
    count = 3
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 16
    t14 = 3
------------------------
#55 pth[3] store count
22: count++;
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 17
------------------------
#56 pth[3] load count
23: if (count == N) {
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 18
    t15 = 4
------------------------
#57 pth[3] tau
23: if (count == N) {
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 19
------------------------
#58 pth[3] broadcast cv
24: pthread_cond_broadcast(&cv);
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 20
------------------------
#59 pth[3] unlock m
30: pthread_mutex_unlock(&m);
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 25
------------------------
#60 pth[3] lock m2
41: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m <unlocked>
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 26
------------------------
#61 pth[3] load b
42: b++;
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m <unlocked>
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 27
    t11 = 0
------------------------
#62 pth[3] store b
42: b++;
------------------------
global vars:
    count = 4
    a = 4
    b = 1
mutex:
    m <unlocked>
    m2 pth[3]
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 28
------------------------

6  条件変数の状態表示

検査の話は以上です.

ここでちょっと,このモデルを借りて,条件変数の状態表示について説明したいと思います.

次のレポート断片は上から切り出してきたものです.スレッド pth[2] が pthread_cond_wait で待ちに入るところです.

------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m pth[2]
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 13
3 pth[2] 23
------------------------
#24 pth[2] wait cv m
27: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 1
    a = 2
    b = 0
mutex:
    m <unlocked>
    m2 pth[1]
thread:
0 main 5
    i = 2
1 pth[0] 10
    arg = 0
2 pth[1] 13
3 pth[2] 24 wait cv
------------------------

待ちに入ったあとの状態を見ると,pth[2] の後ろに wait cv とあります.これが条件変数を待っているという意味です.

ついでにいうと,ミューテックス m のロックが外れています.この2つの動作が同時に(不可分に,アトミックに)起こるところが pthread_cond_wait のポイントですね.

つづいて pthread_cond_broadcast の部分です.このレポートでは最後に到着したスレッドは pth[3] で,それ以外のスレッドはすべて条件変数の待ち状態にあります.そして broadcast 遷移のあとは,全員が待ち状態から脱したことがわかります.

------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24 wait cv
2 pth[1] 24 wait cv
3 pth[2] 24 wait cv
4 pth[3] 19
------------------------
#58 pth[3] broadcast cv
24: pthread_cond_broadcast(&cv);
------------------------
global vars:
    count = 4
    a = 4
    b = 0
mutex:
    m pth[3]
    m2 <unlocked>
thread:
0 main 5
    i = 3
1 pth[0] 24
2 pth[1] 24
3 pth[2] 24
4 pth[3] 20
------------------------

7  まとめ

ミューテックスと条件変数を使ってバリアを作ってみました.その安全性を Pthread Model Checker の機能であるグローバル assert を使って検査しました.グローバル assert は指定された条件をプログラムの実行全体を通して監視してくれる assert です.これを使うと安全性を検査したり,ある条件を満たす状態があるかどうかを調べたりすることができます.

追記: spurious wakeup 対策をしたコードに置き換えました.

2017/10/08

© 2013-2017 PRINCIPIA Limited