Think Stitch
  最近の更新


Pthread Model Checker によるデッドロック検出

Pthread Model Checker の紹介その2です.(その1はこちら

今回はデッドロック検出の例を紹介します.

0  2リソース問題

排他処理が必要なリソースが2つあるとします.たとえばネットワーク上で共有されているスキャナとプリンタという感じで.どちらも使うときにはロックをかけて,使い終わったらアンロックするということになります.

これを同時に使いたいと考えているスレッドが2つあります.このスレッドの振る舞いをモデル化してみます.

1  モデル

モデルのコードは次のように書きました. 2つのリソースをそれぞれ排他制御するためにミューテックスを2つ用意します.

各スレッドとも2つのミューテックスを両方ロックしてからリソースを使用し,終わったらアンロックします.実際にリソースを使う部分はコメントだけにしてあります.ここでは排他制御の構造だけに注目したいので,その部分を抽象化しているということです.

ここでポイントになるのは2つのミューテックスをロックする順番です.すでに知っている人が多いでしょうから,少々わざとらしいですけれども,スレッド1と2でロックをかける順番を逆にしてあります.

two-resources.c

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

pthread_t pth1, pth2;
pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;

void *thread1(void *arg)
{
    pthread_mutex_lock(&m1); // ###
    pthread_mutex_lock(&m2);
    // use resources here
    pthread_mutex_unlock(&m2);
    pthread_mutex_unlock(&m1);
    return NULL;
}

void *thread2(void *arg)
{
    pthread_mutex_lock(&m2); // ###
    pthread_mutex_lock(&m1);
    // use resources here
    pthread_mutex_unlock(&m1);
    pthread_mutex_unlock(&m2);
    return NULL;
}

int main(void)
{
    pthread_create(&pth1, NULL, &thread1, NULL);
    pthread_create(&pth2, NULL, &thread2, NULL);
    pthread_join(pth1, NULL);
    pthread_join(pth2, NULL);
    return 0;
}

2  変換

モデルを変換します.

$ ptmc two-resources.c two-resources.ptmc.c

3  状態遷移グラフ

先に状態遷移グラフを見てみましょう.

$ dot -T png -o two-resources.png two-resources.c.dot

こんなふうになりました.真ん中が main スレッドですね.

4  検査

コンパイルして実行すると,デッドロックがあるといわれます.特に何かオプション等を指定しなくても,Pthread Model Checker はデッドロックを必ず検査してくれます.

$ gcc -o two-resources two-resources.ptmc.c -L libpath -lptmc
$ ./two-resources
deadlock detected
$

5  レポートの解析

レポートは次のようになりました.

two-resources.c.report

version: 1.0.0
model_filename: "two-resources.c"
num_workers: 1
heap_size: 1073741824 bytes
hashtable_size: 4000037 entries
deadlock detected
num-of-states: 14
time: 31 ms
heap: 1024 bytes

#0 main nil
------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 <unlocked>
thread:
0 main 1
------------------------
#1 main create pth1
31: pthread_create(&pth1, NULL, &thread1, NULL);
------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 <unlocked>
thread:
0 main 2
1 pth1 11
    arg = 0
------------------------
#2 main create pth2
32: pthread_create(&pth2, NULL, &thread2, NULL);
------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 <unlocked>
thread:
0 main 3
1 pth1 11
    arg = 0
2 pth2 6
    arg = 0
------------------------
#3 pth2 lock m2
22: pthread_mutex_lock(&m2); // ###
------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 pth2
thread:
0 main 3
1 pth1 11
    arg = 0
2 pth2 7
------------------------
#4 pth1 lock m1
13: pthread_mutex_lock(&m1); // ###
------------------------
global vars:
mutex:
    m1 pth1
    m2 pth2
thread:
0 main 3
1 pth1 12
2 pth2 7
------------------------

順番に見ていきます.まず初期状態です.今回はミューテックスがあるので,ミューテックスの状態が表示されています.ロックされていないミューテックスは <unlocked> と表示されます.

------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 <unlocked>
thread:
0 main 1
------------------------

main スレッドが2つのスレッド pth1, pth2 を生成したあと,まず pth2 が m2 をロックします.ロックされたミューテックスには,オーナーであるスレッドの名前が表示されます[*A].

------------------------
#3 pth2 lock m2
22: pthread_mutex_lock(&m2); // ###
------------------------
global vars:
mutex:
    m1 <unlocked>
    m2 pth2                 <-- [*A]
thread:
0 main 3
1 pth1 11
    arg = 0
2 pth2 7
------------------------
#4 pth1 lock m1
13: pthread_mutex_lock(&m1); // ###
------------------------
global vars:
mutex:
    m1 pth1
    m2 pth2
thread:
0 main 3
1 pth1 12
2 pth2 7
------------------------

つづいてスレッド pth1 がミューテックス m1 をロックしました.この時点でスレッド pth1 は状態 12,pth2 は状態 7 にいます.状態遷移グラフを見ると,それぞれ次の遷移はミューテックスのロックだけです.しかしどちらのミューテックスもすでにロックされていますから遷移できません.ここでデッドロックしてしまうというわけです.

6  問題の修正

複数のミューテックスを入れ子にしてロックする場合には,順番をそろえないとデッドロックしてしまうことがわかりました.そこでモデルを次のように修正します.

two-resources2.c

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

pthread_t pth1, pth2;
pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;

void *thread1(void *arg)
{
    pthread_mutex_lock(&m1); // ###
    pthread_mutex_lock(&m2);
    // use resources here
    pthread_mutex_unlock(&m2);
    pthread_mutex_unlock(&m1);
    return NULL;
}

void *thread2(void *arg)
{
    pthread_mutex_lock(&m1);
    pthread_mutex_lock(&m2); // ###
    // use resources here
    pthread_mutex_unlock(&m2);
    pthread_mutex_unlock(&m1);
    return NULL;
}

int main(void)
{
    pthread_create(&pth1, NULL, &thread1, NULL);
    pthread_create(&pth2, NULL, &thread2, NULL);
    pthread_join(pth1, NULL);
    pthread_join(pth2, NULL);
    return 0;
}

これで問題が解消されました.

$ ptmc two-resources2.c two-resources.ptmc2.c
$ gcc -o two-resources2 two-resources2.ptmc.c -L libpath -lptmc
$ ./two-resources2
$

7  まとめ

Pthread Model Checker によるデッドロック検査の例を紹介しました.

デッドロック検査といっても特に何か手続きが必要なわけではなく,自動的に検査してくれます.状態遷移グラフと合わせてレポートを読むと,デッドロックが発生してしまう理由がわかりやすいと思います.

2017/10/08

© 2013-2017 PRINCIPIA Limited