博士

ロボ子、今日はTLA+を使ったglibcの条件変数のバグ調査について話すのじゃ。

ロボ子

条件変数のバグですか。それは大変ですね。TLA+はプログラムの検証に使う言語でしたっけ？

博士

そうじゃ。TLA+はプログラムの実行を網羅的にチェックして、アサーションが満たされない最短パスを特定できるのじゃ。今回のバグはglibcの条件変数（pthread_cond_signal()）でwake-upが発生しないというものじゃ。

ロボ子

複数の言語に影響する可能性があるんですね。原因は何だったんですか？

博士

コードの複雑さとバグの理解の難しさじゃ。そこで、TLA+を使ってこのバグを調査し、再現に成功したのじゃ。

ロボ子

TLA+で再現できたのはすごいですね！具体的にはどのように？

博士

まず、ミューテックス、Futex、条件変数のプリミティブをTLA+で実装して理解を深めたのじゃ。スピンロックとか、Futexを用いたミューテックスとかも作ったぞ。そして、相互排他とデッドロックからの自由を検証したのじゃ。

ロボ子

なるほど。でも、プロセスの数が増えると状態数が爆発的に増加するんですよね？

博士

その通り！そこが難しいところじゃ。glibcの条件変数の実装は複雑で、6つのFutexを使っているらしいぞ。過去に完了したsignal()呼び出しによってwait()呼び出しがwake upされないようにするためじゃ。

ロボ子

6つも！それは複雑ですね。wrefs, g_refs, g_size, g_signalsといった複数のカウントも使われているんですね。

博士

そうじゃ。特定の条件下でこれらのカウントが不整合になり、バグが発生するのじゃ。TLA+でglibcの条件変数のコードを簡略化してモデル化し、バグを再現したところ、最短パスは209ステップだったぞ。

ロボ子

209ステップ！長いですね。バグの原因は何だったんですか？

博士

プロセスがスリープ状態になる前にsignalが消費された場合に、g_signalsとg_sizeの不整合が発生することが原因じゃ。

ロボ子

なるほど。修正案はあるんですか？

博士

バグレポートのパッチを適用するとか、cv_broadcast()を呼び出すとか、g_signalsにグループのローテーションに関する情報を組み込むとか、Worker 1が早期にcv_wait()から抜けるのを防ぐために、スリーパーとして登録させるとか、色々考えられるのじゃ。

ロボ子

色々ありますね。TLA+は複雑な現実世界のコードを検証するのに役立つんですね。

博士

そうじゃ。コードの簡略化、アサーションの活用、PlusCalによるC++への翻訳が有効じゃ。課題は、長いトレースの解析と状態数の爆発的な増加じゃけどな。

ロボ子

同期プリミティブやプロトコルを検証するのにも非常に有効なんですね。勉強になります！

博士

ところでロボ子、TLA+でバグを見つけるのは、まるで宝探しみたいじゃな。でも、バグが多すぎて、まるでゴミ捨て場みたいじゃ！