SPIN-Modellchecker löst das Weihnachtsmann-Rätsel der nebenläufigen Programmierung
Solving Santa Claus Puzzle
Das Santa-Claus-Nebenläufigkeitsrätsel stellt eine klassische Synchronisationsherausforderung dar: Weihnachtsmann schläft, bis entweder alle neun Rentiere oder drei von zehn Elfen bereit sind, wobei Rentiere Vorrang haben. Der Autor zeigt anhand von drei fehlerhaften Modellen in Promela, wie leicht man das Rätsel falsch löst – etwa wenn Santa mit weniger als neun Rentieren liefert oder gleichzeitig mit Elfen spricht. Anschließend präsentiert er ein korrektes Modell und validiert es mit dem Model Checker SPIN, der alle möglichen Interleavings abdeckt und so Bugs aufdeckt, die Tests übersehen würden.
Die Antwort ist Abdeckung: Ein Model Checker untersucht Interleavings, die Tests oder Experimente übersehen könnten, und beweist entweder Korrektheit oder liefert ein Gegenbeispiel.