サンタクロースのパズルを解く

モデルチェッカーでサンタクロースの並行処理パズルを解く方法 2026年1月10日 本を読むとき、私はしばしば同じ著者の他の作品を探します。Ben-Ariの本を読んでいたとき、彼の他の著作を調べたところ、サンタクロースの並行処理パズルに関する論文1を見つけました。パズルは次のように述べられています。 サンタクロースは、9頭のトナカイすべて、または10頭のエルフのうち3頭のグループによって起こされるまで北極で眠っています。彼は2つの分割不可能なアクションのいずれかを行います。 トナカイのグループによって起こされた場合、サンタはそれらをそりに繋ぎ、おもちゃを配達し、最後にトナカイを外して休暇に出します。 エルフのグループによって起こされた場合、サンタは彼らをオフィスに案内し、おもちゃの研究開発について相談し、最後に彼らを外に出して仕事に戻らせます。 待機中のトナカイのグループは、待機中のエルフのグループよりも先にサンタによって対応されなければなりません。サンタの時間は非常に貴重なので、グループを編成することはサンタが行ってはなりません。 このパズルは、複数のプロセスが調整する必要がある場合に発生する同期の課題を捉えています。私はモデルチェッカーを使ってその正しさを検証したいと思いました。これは簡単な問題だと予想していました。驚いたのは、間違えるのがいかに簡単かということです。 また、解決策へのアプローチも変えました。正しいモデルを書く前に、誤った設計がどのようなものになるかをしばらく探求しました。失敗は教訓的だと感じます。なぜなら、それらは安全でない仮定を露呈し、正しい解決策が何を防止しなければならないかを明確にするからです。学習演習として、それぞれ異なる失敗シナリオを再現する3つの小さなモデルを作成し、正しさのプロパティを使用してバグを検出しました。これらの失敗については後で説明します。その後、正しいモデルを提示し、モデルチェッカーで検証します。 この分析を実行するために、SPINモデルチェッカーを使用し、SPINの仕様言語であるPromelaでモデルを作成しました。 なぜPythonやGoでソリューションを書くのではなく、モデルチェッカーを使用するのかという自然な疑問があります。答えはカバレッジです。モデルチェッカーは、テストや実験では見逃される可能性のあるインターリービングを探索し、正しさを証明するか、反例を生成します。 パズルの3つの重要な制約を見てみましょう。 サンタは自分でグループを編成してはなりません。 トナカイとエルフの両方が待機している場合、サンタはまずトナカイに対応しなければなりません（クリスマスの配達は重要です）。 サンタがグループに対応するとき、グループ全体が一緒に参加しなければなりません。つまり、配達には正確に9頭のトナカイ、相談には正確に3頭のエルフが必要です。例えば、サンタは7頭のトナカイで配達したり、2頭のエルフと相談したりすることはできません。 最初は、問題は単純に見えます。9頭のトナカイが到着するか、3頭のエルフが到着するまで待ち、サンタを起こし、作業を行い、繰り返します。数個のカウンターやロックがあれば十分だと考えがちです。難しさはインターリービングにあります。段階的に推論すると正しく見えるソリューションでも、操作が予期しない方法でインターリーブされると失敗する可能性があります。 それでは、サンタが誤ってパズルを解決する3つの失敗シナリオを考えてみましょう。 サンタは、9頭未満のトナカイしか準備できていないのに、おもちゃを配達してしまう。 微妙なインターリービングの下で、サンタは現実世界では不可能なことを行ってしまいます。それは、おもちゃを配達すると同時にエルフと相談することです。 サンタは、9頭のトナカイがすでに待機して準備ができているにもかかわらず、エルフと相談することを選択する。 これらの失敗シナリオをそれぞれ見てから、すべてのパズルの制約を満たす解決策に向けて進みます。その前に、Promelaで必要となる概念を簡単に紹介します。チャネル、オプション、ガードです。 プロセス間で通信するために、Promelaではチャネルを使用します。チャネルは、送信と受信の2つの操作をサポートするデータ型です。チャネルは、指定された型のメッセージを送信者から受信者に転送します。 SPINは2種類のチャネルをサポートしています。レンデブーチャネルとバッファ付きチャネルです。レンデブーチャネルでは、送信と受信が同期します。送信者は受信者が準備できるまでブロックされ（逆も同様）、転送は1つのアトミックなハンドシェイクとして行われます。バッファ付きチャネルは、プロセスがまだ受信する準備ができていなくても、一時的にメッセージを保持できます。バッファ付きチャネルは、送信者が受信者よりも先に実行することを許可します。レンデブーチャネルは、それらを一緒に動くことを強制します。 送信操作は、チャネル変数に感嘆符（!）と、メッセージの型と一致する必要がある式を続けたものです。対照的に、受信操作は、チャネル変数に疑問符（?）と、メッセージを受信する変数を続けたものです。 例えば、バイト型のメッセージを運ぶレンデブーチャネルを次のように宣言できます（レンデブーチャネルの容量は[0]構文で示されるように0です）。 chan request = [0] of { byte }; 次のようにこのチャネルにデータを送信できます。 request ! 1 そして次のようにデータを受信できます。 byte client; request ? client 次に、オプションとガードについて少し説明します。Promelaのオプションは、コードで分岐を行うために使用できます。例えば、Promelaでif文を次のように書くことができます。 if :: (a < 50) -> printf("a < 50\n"); :: (a > 50) -> printf("a > 50\n"); fi ::で始まる各行はオプションです。オプションは、ガードとアクションで構成されます。ガードは矢印（->）の前のブール式です。オプションは、そのガードが真と評価された場合に有効になります。 if文に到達したとき： 正確に1つのオプションが有効な場合、Promelaはそのオプションを選択します。 複数のオプションが有効な場合、SPINはいずれかを選択する可能性があります（非決定的に）。 オプションが有効でない場合、プロセスはそのifでブロックされます。 それでは、サンタが9頭のトナカイが準備できる前に玩具を配達してしまう可能性のある最初の失敗シナリオを見てみましょう。失敗モデルでは、状態空間を小さく保つために、エルフの数を（例えば3に）縮小することがあります。失敗のメカニズムは同じです。 最初の失敗シナリオをシミュレートするモデルからのコード抜粋を次に示します。 #define NUM_REINDEER 9 #define NUM_ELVES 3 // バッファ付きチャネル chan harnessed = [NUM_REINDEER] of { bit }; chan done_consulting = [NUM_ELVES] of { bit }; // コードの簡略化のため省略 active [NUM_REINDEER] proctype Reindeer() { do :: r_arrive ! 1; harnessed ? 1; actually_harnessed++; actually_harnessed--; od } active proctype Santa() { byte i = 0; byte e = 0; byte j; do :: (i < NUM_REINDEER) -> r_arrive ? 1; i++; if :: (i == NUM_REINDEER) -> reindeer_ready = true :: else -> skip fi :: (i == NUM_REINDEER) -> for (j : 1 .. NUM_REINDEER) { harnessed ! 1; } delivering = true; /* おもちゃ配達のシミュレーション */ delivering = false; reindeer_ready = false; i = 0; // コードの簡略化のため省略 - 完全なコードは以下でリンクされています od } // 正しさのプロパティ ltl safety { [] (delivering -> actually_harnessed == NUM_REINDEER) } このPromelaモデルは、サンタの問題の小さな「実行可能な仕様」です。モデル全体と実行方法の説明は、リポジトリ2で入手できます。単純にするために、主にサンタとトナカイのやり取りについて説明します。エルフは、全体的な構造を似たものにするためにのみ存在します。 active [N] proctype P(){…} という構文は、SPINにプロセスPのN個の並行コピーを初期状態で開始するように指示します。したがって、ここでは9頭のトナカイプロセス、3頭のエルフプロセス、および1頭のサンタプロセスが得られます。各トナカイはr_arriveチャネルでレンデブー送信をループします。つまり、サンタが受信するまでブロックされ、その後harnessedでハーネスメッセージを待ちます。サンタはループし、トナカイの到着を数えます。9頭すべてのトナカイが到着すると、彼はharnessedで9つのメッセージを送信してそれらを「ハーネス」し、その後briefly delivering = trueを設定しておもちゃの配達を表します。 バグは、harnessedがバッファ付きチャネルであるため、サンタは9つのハーネスメッセージすべてをキューに入れ、すぐに続行できることです。これにより、トナカイが実際にそれらを受信することを強制するものは何もありません。これは、サンタがグループ全体が一緒に参加して配達しなければならないというパズルの制約に違反します。この実装がパズルの制約を尊重しているかどうかを確認するために、線形時相論理（LTL）で正しさのプロパティを記述します。 簡単に言えば、