How to Solve Santa Claus Concurrency Puzzle with a Model Checker | Waqas Younas' blog Waqas Younas' blog<br>How to Solve Santa Claus Concurrency Puzzle with a Model Checker<br>Jan 10, 2026<br>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 1. The puzzle is stated as follows:<br>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:<br>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.<br>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.<br>To carry out this analysis, I used the SPIN model checker and wrote the models in Promela, SPIN’s specification language.<br>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.<br>Let’s look at three key puzzle constraints:<br>Santa must not marshal the groups himself.<br>If both reindeer and elves are waiting, Santa must serve the reindeer first (Christmas delivery is critical).<br>When Santa serves a group, the entire group must participate together: exactly nine reindeer for delivery, or exactly three elves for consultation. Santa cannot deliver toys with seven reindeer or consult with two elves, for example.<br>At first, the problem seems straightforward. You wait until nine reindeer arrive or three elves arrive, wake Santa, do the work, and repeat. It is tempting to think that a few counters or locks are enough to solve it. The difficulty is in the interleavings. A solution that appears correct when reasoning step by step can fail when operations interleave in unexpected ways.<br>Let’s now consider three failure scenarios that solve the puzzle incorrectly.<br>Santa delivers toys even though fewer than nine reindeer are actually ready.Under a subtle interleaving, Santa ends up doing something impossible in the real world: delivering toys and consulting with elves at the same time.Santa chooses to consult with elves even though nine reindeer are already waiting and ready to go.We’ll look at each of these failure scenarios next, and then work toward a solution that satisfies all puzzle constraints. Before that, let’s briefly introduce the Promela concepts we’ll need: channels, options, and guards.<br>To communicate between processes, we use channels in Promela. A channel is a data type that supports two operations: send and receive. Channels transfer messages of a specified type from a sender to a receiver.<br>SPIN supports two kinds of channels: rendezvous channels and buffered channels. In a rendezvous channel, send and receive synchronize: the sender blocks until the receiver is ready (and vice versa), and the transfer occurs as one atomic handshake. Buffered channels can hold messages temporarily, even if no process is ready to receive them yet. Buffered channels let a sender run ahead of a receiver; rendezvous channels force them to move together.<br>A send operation consists of a channel variable followed by an exclamation mark (!) and a sequence of expressions whose number and types must match the channel’s message type. A receive operation, by contrast, consists of a channel variable followed by a question mark (?) and a sequence of variables into which the message is received.<br>For example, we can declare a rendezvous channel named request that carries messages of type byte as follows (rendezvous channels have capacity of 0 as indicated by [0] syntax):<br>chan request = [0] of { byte };
We can send data on this channel as:<br>request ! 1<br>and receive data as:<br>byte...