SPINモデルチェッカーで解くSanta Claus並行パズル

Solving Santa Claus Puzzle

Santa Claus並行パズルは、複数のプロセスが協調する際の同期の難しさを示す古典的な問題です。著者はSPINモデルチェッカーとPromela言語を使ってこのパズルを検証し、一見正しそうな実装が微妙なインターリービングで失敗することを発見しました。3つの失敗シナリオ（9頭未満のトナカイでの配達、配達と相談の同時発生、待機中のトナカイを無視したエルフへの対応）をモデル化し、LTLプロパティでバグを検出。最終的に正しいモデルを提示し、モデルチェッカーの網羅性がテストや実験では見つけられない問題を明らかにすることを示します。