How to Solve Santa Claus Concurrency Puzzle with a Model Checker
Jan 10, 2026
When I enjoy a book, I often look for other work by the same author. While reading a book by Ben-Ari, I looked up his other writing and came across a paper on the Santa Claus concurrency puzzle . The puzzle is stated as follows:
Santa Claus sleeps at the North Pole until awakened by either all nine reindeer or a group of three out of ten elves. He performs one of two indivisible actions: If awakened by the group of reindeer, Santa harnesses them to a sleigh, delivers toys, and finally unharnesses the reindeer, who then go on vacation.
If awakened by a group of elves, Santa shows them into his office, consults with them on toy R&D, and finally shows them out so they can return to work constructing toys. A waiting group of reindeer must be served by Santa before a waiting group of elves. Since Santa’s time is extremely valuable, marshalling the reindeer or elves into a group must not be done by Santa.
The puzzle captures the kind of synchronization challenges that arise whenever multiple processes must coordinate. I wanted to validate its correctness using a model checker. I expected this to be a simple problem. What surprised me is how easy it is to get it wrong.
I also chose a different path to the solution. Before writing the correct model, I spent some time exploring what incorrect designs might look like. I find failures instructive because they expose unsafe assumptions and make clear what a correct solution must prevent. As a learning exercise, I wrote three small models, each reproducing a different failure scenario, and used correctness properties to catch the bugs. We will look at these failures in a bit. After that, I present the correct model and validate it with a model checker.
To carry out this analysis, I used the SPIN model checker and wrote the models in Promela, SPIN’s specification language.
A natural question is why use a model checker instead of simply writing the solution in Python or Go. The answer is coverage: a model checker explores interleavings that tests or experiments might miss, and either proves correctness or produces a counterexample.
Let’s look at three key puzzle constraints:
... continue reading