How to Solve Santa Claus Concurrency Puzzle with a Model Checker

Jan 10, 2026When 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: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:Santa must not marshal the groups himself.

If both reindeer and elves are waiting, Santa must serve the reindeer first (Christmas delivery is critical).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.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.Let’s now consider three failure scenarios that solve the puzzle incorrectly.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.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.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.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.

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):chan request = [0] of { byte }; We can send data on this channel as:request ! 1 and receive data as:byte client; request ? client Now a few words about options and guards. Options in Promela can be used to do branching in the code. For example, one could write an if statement in Promela as:if :: (a < 50) -> printf("a < 50\n"); :: (a > 50) -> printf("a > 50\n"); fi

Each line beginning with :: is an option. An option consists of a guard followed by an action. The guard is the Boolean expression before the arrow (->). An option is enabled if its guard evaluates to true.When the if statement is reached:if exactly one option is enabled, Promela takes that option;if multiple options are enabled, SPIN may choose any one of them nondeterministically;if no option is enabled, the process blocks at the if.Now let’s look at the first failure scenario in which Santa may deliver toys without all nine reindeer being ready. In the failure models I sometimes shrink the number of elves (e.g., to 3) to keep the state space small; the failure mechanism is the same.Here is a code excerpt from the model that simulates the first failure scenario:#define NUM_REINDEER 9 #define NUM_ELVES 3

// buffered channels chan harnessed = [NUM_REINDEER] of { bit }; chan done_consulting = [NUM_ELVES] of { bit };

// Some code omitted for brevity

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; /* simulating delivering toys */ delivering = false; reindeer_ready = false; i = 0; // Some code omitted for brevity - complete code linked below }

// Correctness property ltl safety { [] (delivering -> actually_harnessed == NUM_REINDEER) } This Promela model is a small “executable spec” of the Santa problem. The full model and instructions for running it are available in the repository 2. To keep things simple, I mainly discuss the Santa–reindeer interaction; elves are present only to keep the overall structure similar.The syntax active [N] proctype P(){…} tells SPIN to start N concurrent copies of process P in the initial state, so here you get 9 Reindeer processes, 3 Elves processes, and 1 Santa process.

In other words, Santa starts delivering toys while some reindeer are still unharnessed. The property fails, and SPIN produces a counterexample showing exactly how this execution occurs. The code shows this model, along with instructions for running it and viewing the trace that contains the counterexample.Now let’s look at a second failure scenario, in which Santa may end up doing the seemingly impossible, delivering toys with the reindeer and consulting with the elves at the same time. The complete model that simulates this fault is available here 3; an excerpt is shown below.To make this bug easy to trigger, I did something silly: I split Santa into two: one responsible for toy delivery and one for consultation. Each process independently waits for its own group to form and then sets the corresponding flag (delivering or consulting) to indicate that work has begun. Because these two processes run concurrently and share no mutual exclusion, there exists an interleaving in which both flags become true at the same time.The code violates a core constraint of the puzzle: Santa must perform only one indivisible action at a time. By adding an assert statement that asserts Santa never delivers and consults simultaneously, SPIN is able to find a concrete counterexample trace showing exactly how this impossible situation arises under a particular interleaving. active proctype SantaConsulting() {

byte e = 0; byte j; end: do :: (e < NUM_ELVES) -> e_arrive ? 1; e++; :: (e == NUM_ELVES) ->

consulting = true; assert !(consulting && delivering); // We release elves here consulting = false; e = 0; od

} active proctype SantaToyDelivery() { byte i = 0; byte j=0; end: do :: (i < NUM_REINDEER) -> r_arrive ? 1; i++; :: (i == NUM_REINDEER) -> delivering = true; // We release the reindeer here delivering = false; i = 0; od }

// correctness property

ltl reindeer_precedence { [] ( (r_count == NUM_REINDEER) -> ( (!