uchan note

プログラミングや電子工作の話題を書きます

ベクタークロックと競合検査

C++ プログラム解析

ベクタークロック（vector clock）という名前は，クロック（時計）を並べたベクターというところからきています。 マルチスレッドプログラムの競合検査の分野で言うベクタークロックは，各スレッドの論理時刻を並べたものです。

uchan がベクタークロックをちょっと勉強したので，メモがてら解説を書いてみます。 最終的に，競合状態を検出する実例を示すところまでをゴールとします。

競合検査

競合検査とは，マルチスレッドプログラムに潜むデータ競合（dara-race）や競合状態（race condition）の有無を検査することです。 ベクタークロックは主に競合状態の検査に使われると uchan は認識しています。 データ競合と競合状態の違いは データ競合(data race)と競合状態(race condition)を混同しない - Qiita が分かりやすかったです。 この記事にもある通り，意図した競合状態はバグではありませんが，競合検査では通常，それが意図的かどうかは分からないのですべての競合状態を検査対象とします。

具体的には次のプログラムにはデータ競合はありませんが競合状態があります。

#include <atomic>
#include <iostream>
#include <thread>

std::atomic<int> x{0};
const int kCount = 100000;

void f() {
  for (int i = 0; i < kCount; ++i) {
    int tmp = x.load();
    x.store(tmp + 1);
  }
}

int main() {
  std::thread th1{f};
  std::thread th2{f};
  th1.join();
  th2.join();
  std::cout << "expected = " << 2 * kCount
            << ", actual = " << x.load() << std::endl;
}

筆者の環境でコンパイル，実行すると次のような結果を得ました。

$ clang++ -Os a.cpp -lpthread
$ ./a.out 
expected = 200000, actual = 99306

expected より actual が小さくなっていて，意図しない競合状態が起きていることが分かります。（思ったより小さい値になってびっくりしました）

happens-before 関係

競合状態を防ぐ典型的な手法は，何らかの同期機構を使ってクリティカルセクション，ここでは x.load() から x.store() までの区間に同時に侵入できるスレッドを 1 つに限定することです。 同期機構として有名なのはミューテックスやモニタです。 いずれにせよ，競合状態を解消するには x.load() から x.store() までの区間があるスレッドによって実行されている間は，他のスレッドがこの区間に侵入しないように制御する必要があります。 ミューテックスを使うと次のようになります。

#include <atomic>
#include <iostream>
#include <mutex>
#include <thread>

std::atomic<int> x{0};
const int kCount = 100000;
std::mutex m;

void f() {
  for (int i = 0; i < kCount; ++i) {
    m.lock();
    int tmp = x.load();
    x.store(tmp + 1);
    m.unlock();
  }
}
…略

クリティカルセクションに入る前にミューテックスをロック（acquire）し，クリティカルセクションから出た後にミューテックスをアンロック（release）します。 この改造により，expected == actual となります。

競合状態の有無を形式的に記述したいときに使うものが happens-before 関係です。 A と B の間に happens-before 関係があるとは，A が かならず B より先に起きる，ということです。 たまたま A が B より先に起きた（スレッドスケジューリングによっては逆転する）ようなケースでは happens-before 関係があるとは言いません。

ミューテックスを使った例では次の 4 種類の happens-before 関係があります。

  • 同一スレッド内で m.lock() は m.unlock() より前に起きる。
    • なぜならなぜなら関数 f 内でそのような順で書いてあるから1。
  • 先に実行されたスレッドの m.unlock() は，後に実行されたスレッドの m.lock() より先に起きる。
    • なぜなら，後に実行されたスレッドの m.lock() は m.unlock() が実行されるまでブロックされるから。
  • スレッド N の生成はスレッド N の実行開始より前に起きる。
  • スレッド N の実行終了は thN.join() より前に起きる。

2 つの happens-before 関係から，次のような happens-before 関係の遷移を考えることができます。「→」を happens-before 関係を表す矢印とします。

  • スレッド A の m.lock() → スレッド A の m.unlock() → スレッド B の m.lock() → スレッド B の m.unlock() → スレッド A の m.lock() → …
  • スレッド A の m.lock() → スレッド A の m.unlock() → スレッド A の m.lock() → スレッド A の m.unlock() → スレッド B の m.lock() → …

これですべてではありませんが，いずれの遷移でもクリティカルセクションが並行に実行されることはない，ということが分かります。

happens-before 関係が無い場合，それらは並行（concurrent）に実行されます。happens-before 関係があれば，それらは順次実行されます。

ベクタークロック

ベクタークロックは happens-before 関係が無い，つまり並行に実行される変数の読み書きを検出するのに使える道具の 1 つです。 スレッドの個数分の要素を持つベクターを各スレッドが保有し，そのクロックをルールに従って更新していくことで happens-before 関係が成り立たない変数の読み書きを検知することができます。

アルゴリズムによってベクタークロックの作り方や値の更新の仕方が変わります。 それは，各アルゴリズムが検知する対象が異なるからです。

この記事ではグローバル変数の read と write，および write と write の間に競合状態があることを検出する手法である Djit+2 のアルゴリズムにおけるベクタークロックを紹介します。 といいつつ，実際は Djit+ のアルゴリズムを意味が変わらない範囲で改良したアルゴリズム3 に基づいて紹介します。

初期値

各スレッドは，自分のスレッド番号に対応する要素だけが 1，他の要素は 0 であるような初期値のベクタークロック C を持ちます。 先の例では 2 つのスレッドが次のような初期ベクタークロックを持ちます。

  • C1 = <1, 0>
  • C2 = <0, 1>

スレッド間で共有される変数に対して，スレッドの個数分の要素を持つベクタークロック R，W を用意します。 先の例ではそのような変数は x だけですので，用意するベクタークロックは 2 つ（Rx と Wx）です。

  • Rx = <0, 0>
  • Wx = <0, 0>

各ロック変数に対して，スレッドの個数分の要素を持つベクタークロック L を用意します。 先の例ではロック変数は m だけです。

  • Lm = <0, 0>

これらのベクタークロックの意味を直感的に考えると，次のようなものです。

  • C：各スレッド視点での全スレッドのクロックの値。スレッド間で同期操作をしたときにだけ各要素の値が更新されていく。（同期しないかぎり他のスレッドの状態は不可視であり，クロック値は更新されない。）
  • R，W：各スレッドが最後に変数を読み書きしたときのスレッド時刻。
  • L：各スレッドが最後にロックを解放（release）したときのスレッド時刻。

更新ルール

Djit+ のアルゴリズムでは 4 つの操作に注目して解析を行います。

  • rel(t, m)：スレッド t がロック m を解放する
  • acq(t, m)：スレッド t がロック m を取得する
  • rd(t, x)：スレッド t が変数 x を読む
  • wr(t, x)：スレッド t が変数 x に書く

それぞれの操作では，次のルールに従ってベクタークロックを更新します。

  • rel(t, m)
    1. Ct(t) ← Ct(t)+1（Ct の中の t 番目の要素だけを 1 増やす）
    2. Lm ← Ct
  • acq(t, m)
    1. すべての u に対して Ct(u) ← max(Ct(u), Lm(u))
  • rd(t, x)
    1. Rx(t) ← Ct(t)（Rx の t 番目に Ct の t 番目を代入する）
  • wr(t, x)
    1. Wx(t) ← Ct(t)（Wx の t 番目に Ct の t 番目を代入する）

実例：ミューテックスあり版

ミューテックスがある方のプログラムが，スレッド 1，スレッド 2 の順に動作するとします。このとき 4 つの操作が次の順に実行されます。

acq(1, m) → rd(1, x) → wr(1, x) → rel(1, m) → acq(2, m) → rd(2, x) → wr(2, x) → rel(2, m)

このとき，ベクタークロックの値の変化は次の通りです。（変化した数値を 1 のように協調しています）

C1 C2 Rx Wx Lm
初期状態 <1,0> <0,1> <0,0> <0,0> <0,0>
acq(1, m) <1,0> <0,1> <0,0> <0,0> <0,0>
rd(1, x) <1,0> <0,1> <1,0> <0,0> <0,0>
wr(1, x) <1,0> <0,1> <1,0> <1,0> <0,0>
rel(1, m) <2,0> <0,1> <1,0> <1,0> <2,0>
acq(2, m) <2,0> <2,1> <1,0> <1,0> <2,0>
rd(2, x) <2,0> <2,1> <1,1> <1,0> <2,0>
wr(2, x) <2,0> <2,1> <1,1> <1,1> <2,0>
rel(2, m) <2,0> <2,2> <1,1> <1,1> <2,2>

重要なのは競合状態を検査することです。rd および wr の操作の直後に次の検査を行います。 VC1⊆VC2 は「すべての u について VC1(u)≦VC2(u)」という意味です。

  • rd(t, x)：Wx⊆Ct
  • wr(t, x)：Wx⊆Ct かつ Rx⊆Ct

これが成り立てば競合が無いことを意味します。

例えば，rd(1, x) の直後では C1=<1,0>，Wx=<0,0> ですので，Wx⊆C1 が成り立ちます。 wr(2, x) の直後では C2=<2,1>，Wx=<1,1>，Rx=<1,1> ですので，Wx⊆C2 かつ Rx⊆C2 が成り立ちます。

すべての rd，wr について検査が通過します。つまり，ミューテックスを用いたプログラムでは競合が検出されませんでした。

実例：ミューテックス無し版

ミューテックスが無い方のプログラムが次の順に動作するとします。

rd(1, x) → rd(2, x) → wr(1, x) → wr(2, x)

このとき，ベクタークロックの値の変化は次の通りです。

C1 C2 Rx Wx Lm
初期状態 <1,0> <0,1> <0,0> <0,0> <0,0>
rd(1, x) <1,0> <0,1> <1,0> <0,0> <0,0>
rd(2, x) <1,0> <0,1> <1,1> <0,0> <0,0>
wr(1, x) <1,0> <0,1> <1,1> <1,0> <0,0>
wr(2, x) <1,0> <0,1> <1,1> <1,1> <0,0>

wr(1, x) の直後では C1=<1,0>，Wx=<1,0>，Rx=<1,1> ですので，Wx⊆C1 は成り立ちますが Rx⊆C1 が成り立ちません。 競合が検出されました！

  1. コンパイラや CPU は，そのスレッドにとって意味が変わらない範囲で任意に命令を入れ替える（リオーダ）ことがあるが，ミューテックスなどの同期機構に対する操作に関してはリオーダされないことが保証されている。↩

  2. Pozniansky, E., & Schuster, A. (2003). Efficient on-the-fly data race detection in multithreaded C++ programs. Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003, 179–190. https://doi.org/10.1109/IPDPS.2003.1213513↩

  3. Flanagan, C., & Freund, S. N. (2010). FastTrack: Efficient and precise dynamic race detection. Communications of the ACM, 53(11), 93–101. https://doi.org/10.1145/1839676.1839699↩