Think Stitch
  最近の更新


条件変数の Spurious Wakeups

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

今回は条件変数の spurious wakeups についてです.

先に謝っておくと,特定の実装で spurious wakeups がなぜ起こるのか,という話ではありません.それを期待して検索の結果たどり着いた人,ごめんなさい.逆にご存じの方にはご教示いただきたいと思います.

ここでは仕様の立場に立って検査の話をします.なんにせよ,プログラムは実装ではなく仕様 (interface) に基づいて書く必要があるわけですし.

0  Spurious wakeups

POSIX の規格によると pthread_cond_wait は signal も broadcast も呼ばれていないのに待ち状態から抜けてくることがあるようです.

"Spurious wakeups from the pthread_cond_timedwait() or pthread_cond_wait() functions may occur. Since the return from pthread_cond_timedwait() or pthread_cond_wait() does not imply anything about the value of this predicate, the predicate should be re-evaluated upon such return."

-- 出典 The Open Group Base Specifications Issue 7, IEEE Std 1003.1-2008, 2016 Edition

したがって pthread_cond_wait を使うときには,抜けてきたあとで必ず関連付けている条件を再検査して,もし不成立だったらまた wait しなければならないということです.

次のバリアのコードを見てください(前回の記事の最初の版はこれでした).

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

もし spurious wakeups がないのであれば,pthread_cond_broadcast が呼ばれたときだけ待ち状態 *A から起きてくるわけですからいいはずですが,そうでなくても抜けてしまうのでは困ります.

そこで待ち状態から起きてきたときに,条件を再度確認するようにします:

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);
}

1  Pthread Model Checker の spurious wakeups オプション

Pthread Model Checker の既定の動作としては,spurious wakeups は起こりません.したがって上のモデルはどちらも問題ない(前回記事参照)ということになります.

Pthread Model Checker version 1.1 から spurious wakeups を検査するための機能を追加しました.検査プログラムを実行するときに -s オプションをつけると pthread_cond_wait が spurious wakeups を起こすようになります.

このオプションを使い,上のモデルについて前回の安全性検査をもう1度やってみます. 2番目のモデルは問題ありません.しかし1番目のモデルはグローバル assert に違反します.

$ ./barrier -s
global assertion violation
barrier.c:17: // @ASSERT(b == 0 || a == N)

レポートは次のとおりです:

version: 1.1.0
model_filename: "barrier.c"
num_workers: 1
heap_size: 1073741824 bytes
hashtable_size: 4000037 entries
spurious_wakeups: on
global assertion violation
barrier.c:17: // @ASSERT(b == 0 || a == N)
num-of-states: 1119
time: 32 ms
heap: 82952 bytes

#0 main nil
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 1
------------------------
#1 main tau
48: 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
48: 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]
49: 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 pth[0] lock m2
33: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 11
------------------------
#5 pth[0] load a
34: a++;
------------------------
global vars:
    count = 0
    a = 0
    b = 0
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 12
    t10 = 0
------------------------
#6 pth[0] store a
34: a++;
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 13
------------------------
#7 pth[0] unlock m2
35: pthread_mutex_unlock(&m2);
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 14
------------------------
#8 pth[0] lock m
21: pthread_mutex_lock(&m);
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 15
------------------------
#9 pth[0] load count
22: count++;
------------------------
global vars:
    count = 0
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 16
    t14 = 0
------------------------
#10 pth[0] store count
22: count++;
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 17
------------------------
#11 pth[0] load count
23: if (count == N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 18
    t15 = 1
------------------------
#12 pth[0] tau
23: if (count == N) {
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 20
------------------------
#13 pth[0] wait cv m
26: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 22 wait cv
------------------------
#14 pth[0] spurious-wakeup
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 22
------------------------
#15 pth[0] lock m
26: pthread_cond_wait(&cv, &m);
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m pth[0]
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 21
------------------------
#16 pth[0] unlock m
28: pthread_mutex_unlock(&m);
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 23
------------------------
#17 pth[0] lock m2
39: pthread_mutex_lock(&m2);
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 24
------------------------
#18 pth[0] load b
40: b++;
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 25
    t11 = 0
------------------------
#19 pth[0] store b
40: b++;
------------------------
global vars:
    count = 1
    a = 1
    b = 1
mutex:
    m <unlocked>
    m2 pth[0]
thread:
0 main 5
    i = 0
1 pth[0] 26
------------------------

ポイントになるのは 14 ステップ目で,spurious-wakeup という遷移があります.これによって条件変数 cv を待っていたはずのスレッド pth[0] が待ち状態から抜けてしまっています.結果としてバリアを超えてしまい,assert にひっかかったということです.

------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 22 wait cv
------------------------
#14 pth[0] spurious-wakeup
------------------------
global vars:
    count = 1
    a = 1
    b = 0
mutex:
    m <unlocked>
    m2 <unlocked>
thread:
0 main 5
    i = 0
1 pth[0] 22
------------------------

2  デッドロック検査を目的としている場合

Spurious wakeups オプションをつけると任意の時点で非決定的に待ち状態から抜けてきてしまうので,あるはずのデッドロックが消えてしまうことがあります.たとえば次のモデルをみてください:

pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
pthread_cond_t cv = PTHREAD_COND_INITIALIZER;

int main(void)
{
    pthread_mutex_lock(&m);
    pthread_cond_wait(&cv, &m);
    pthread_mutex_unlock(&m);
    return 0;
}

誰も起こす人がいませんから明らかにデッドロックするモデルですが,spurious wakeups オプション -s をつけるとデッドロックが消えてしまいます.つまり -s オプションをつけると,spurious wakeups が起こりうる状態がずっと続く場合にはいつかは必ず起こるという,やや強い仕様になっています.

したがってデッドロック検査を目的としている場合には spurious wakeups オプション -s をつけないで検査するということです.

3  まとめ

Spurious wakeups と Pthread Model Checker の spurious wakeups オプションについて紹介しました.

Pthread Model Checker で検査を行う場合は,まず spurious wakeups オプションなしで検査をして,デッドロックや assert 違反がないことを確認します.

その後で,もし spurious wakeups があっても問題がないかどうか検査したい場合には spurious wakeups オプションをつけて再度検査するとよいでしょう.

2017/10/09

© 2013-2017 PRINCIPIA Limited