Solvingn the Santa Claus concurrency puzzle with a model checker

a month ago

The Santa Claus concurrency puzzle involves Santa being awakened by either all nine reindeer or a group of three out of ten elves, with reindeer having priority.
Santa performs one of two indivisible actions: delivering toys with reindeer or consulting with elves on toy R&D.
The puzzle's constraints include Santa not marshaling groups himself, prioritizing reindeer over elves, and ensuring full group participation.
A model checker like SPIN is used to explore all possible interleavings and validate correctness, ensuring coverage beyond what tests might miss.
Three failure scenarios are explored: delivering with incomplete reindeer groups, simultaneous delivery and consultation, and consulting despite waiting reindeer.
The correct solution involves separate rooms for reindeer and elves to handle marshaling, with Santa only performing the work after a group is ready.
Safety properties ensure correct group sizes and mutual exclusion, while liveness properties ensure Santa eventually serves pending requests.
The solution is validated using SPIN, with all properties passing, and is also implemented in Go for practical application.

Hasty Briefsbeta