Sound Predictive Race Detection in Polynomial Time

http://users.soe.ucsc.edu/~cormac/papers/popl12a.pdf

あまりきちんと理解できてないけど、ざっと読みました。以下間違ってることが普通にあるかもしれません…

さて、 race detector はむずかしいと思う。本質的に難しいっていうより、なんかあまり他と接点を持たない独特なあれこれが積み上がってて、かつ並列なプログラムっていうのはプログラマの中でも関心を持つ人の割合が少ないドメインだから、かなぁと思う。簡単に言うとなんか渋いジャンルだな…とかいう。というわけで適当な事前知識から。

事前知識

Lock-set な race detector は、メモリのアクセスのたびに、そのメモリの番地とその時確保されてるロックを記録する。同じ番地に対して、べつなスレッドから共通のロックを確保せずにアクセスが起きたら race を報告。ありえるレース全てを報告できるけど、問題点は false-positive が山ほど出ること。

ThreadSanitizer とかは happened-befode (以下HB) っていう、実際に走らせた時に間に fork/join やら signal/wait がはさまった場合は、それらで分離された前と後のイベントは同時に起きないと考えてやりましょ、という情報を加える。これで false-positive が減るけど、でもまだ結構起きる。 lock や lock-free algorithm によって同時に起きないことが保証されてるけど race detector にはわからないコードには適当に annotation なんかを加えて、 HB 関係を明示的に detector に伝えることもできる。

fork/join, signal/wait だけじゃなくて、 lock/unlock も HB 関係と仮定しましょ、っていうモードも ThreadSanitizer にはあって、これはたぶん false-positive がまただいぶ減って大規模なソフトでも気楽に使えるイメージ。が、かなり保守的すぎて、 race を見逃す率が高くなる嫌いがありそう。

概要

上で書いた通り、 lock/unlock も HB と考えるバージョンだと (この論文ではこっちの HB を HB と呼んでるみたいなんで、以下単に HB とします)、たまたま実際に実行した時の順序を過信して本物の race を結構見逃す。具体的な例として、 HB detector で適当なプログラムを走らせてみて、以下のような trace を得たとする。

Event 0: write(x) @ thread 1
Event 1: lock(mu) @ thread 1
Event 2: unlock(mu) @ thread 1
Event 3: lock(mu) @ thread 2
Event 4: unlock(mu) @ thread 2
Event 5: write(x) @ thread 2

Event 2 -> Event 3 には HB 関係が成り立ってるので、 Event 0 の write と Event 5 の write は共通のロックを持ってないものの、 race と報告されない。

これを解決するために、実行 trace の順序を入れ変えまくってみましょ、というのがこの論文の提案。ただ detect できる race の数を増やしつつも false-positive は増やしたくない。そのために causally-preceedes (以下 CP) という、 HB より弱い関係を定義して、その関係が無いところを入れ替える場合は false-positive が増えませんよ、というのが趣旨。

例えば上の例だと、 HB な detector は Event 0 が Event 3 より先に実行されちゃうとうまく race を検出できないのだけど、 CP を使っている detector だと、 Event 2 => Event 3 は CP ではないので、 Event 0-2 と Event 3-5 をひっくりかえしてみてチェックすることができて、ひっくりかえすとモロに race 以外の何者でもないので検出できる、と。

Causally preceedes

定義が 2.1 に書いてある、がこれが HB と違ってややこしくてむつかしい。

thread 1 で lock/unlock => thread 2 で lock/unlock という流れがあって、それぞれの thread のクリティカルセクションに lock がなれば race になってるメモリアクセスがあれば、 thread 1 unlock => thread 2 lock が CP
同じ設定でクリティカルセクション内に CP 関係なイベントがあれば、 thread 1 unlock => thread 2 lock も CP
A <

で、この定義を読むと CP なら HB だなーというのはわかります。ですが、 CP じゃないところを reorder しても現実には絶対ありえない順序を作っちゃうことがないのかがピンと来てないのと、逆に、なんで CP が HB に比べて十分に弱い、つまり reorder してもいいところが CP になっちゃうことが無いのか、がよくわかってません。後者の方は Appendix に長い証明があるようなんですが、読んでません…いやこの証明はちょっと違う話かな…

実装とか

ちなみに Java 。コード無いのかなーと探したけど見つからなくて、商用のもの使ってるらしいんでたぶんリリースされないんだと思う。残念…

CP は結構ややこしいので、 CP であるかをチェックするのは、 trace を一回なめるだけでできるアルゴリズムは見つかってない(つーことは ThreadSanitizer みたいに実行時に warning 出すのはちょっと難しいわけですな)。必要があれば昔のを参照する必要がある、がまぁ多項式時間なアルゴリズムはある。 prolog 系のなんからしい datalog とかいうもので実装したらしい。

HB とか CP を全部のイベントに対して計算するのは大変なので、 unlock-lock のとこだけチェックして、後は必要なとこだけ計算する。まぁこれはそりゃそうかな、と思う。

それやってもまだまだ大変なので、適当なイベントの window サイズ (典型的には 500 から 1000) を設定して、その間でだけ HB と CP を考える、と。まぁそれもそんなもんかなーと思います。これで false-negative がやや出てくる可能性があるわけですね…

あと race が見つかった時に、その後は CP をちゃんと計算できなくなるんで、 false-positive を出さないように保守的に倒して、 race が起きたところを CP edge として考える、と。 race の近くに race がある場合に検出できなくなるかもだけど、まぁ最初の race 修正してから実行すれば検出できるので良いとする。

実験結果

色んなベンチマークとか実アプリとかでやってみました、と。 HB だけのやつに比べて、 2 つだけ CP の方が良かったケースがありました、という少しさみしい結果。まぁ HB より悪いやつはもちろん無い。 HB と同じになるケースとしては、構造が単純で HB があっさり見つけちゃうケースと、実行回数が多いループがあるせいで、 HB が問題のある実行パターンを全部試してしまうケースがある、と。まぁそうだろう。

あと CP が余計に検出できたケースがどういうケースだったかについて言及が無いのも残念。あと window を設定したせいで検出できなかったケースが無かったか、なんかにも言及が無い。

まとめ

なにやら面白いと思う。今まで読んだ race detector の話は、 false-positive 減らすと false-negative が増える感じで、いいとこのバランス取るしかないよね…的な感じだったのに、 false-negative 減らしつつ false-positive が増えないのは画期的感がある気がする。

ただ実装が参照できないのと、実験結果の考察がどうもイマイチ足りてないような…な感じなのが残念だった。

ちょっと手を動かして遊んでみたい分野です…