用 SPIN 模型检查器破解 Santa Claus 并发谜题

Solving Santa Claus Puzzle

我在阅读 Ben-Ari 的著作时发现了经典的 Santa Claus 并发谜题，决定用 SPIN 模型检查器和 Promela 语言来验证其正确性。本以为这很简单，结果却踩了不少坑。我特意先构建了几个错误的模型，模拟了驯鹿不足却发车、同时处理多组任务等失败场景，以此暴露并发中的隐蔽假设。通过对比错误设计与正确方案，我深刻体会到模型检查器在遍历所有线程交错状态方面的独特价值，它能发现传统测试无法捕捉的逻辑漏洞，确保 Santa Claus 严格遵循优先服务驯鹿和全员参与的核心约束。

"我选择了一条不同的解决路径，在编写正确模型之前，我花了一些时间探索错误的设计可能是什么样子。"