**Peterson 算法**：Model checker 给了我们探索 Peterson 算法变体的能力：我们可以改变语句执行的顺序等，实现 Peterson 算法的变体，并且由 model checker 给出一个快速的反馈，在反馈的基础上，我们能更快、更好地理解 Peterson 算法的原理。然而，在宽松内存模型上，Peterson 算法既低效又很难实现。直接用 load/store 实现互斥并不是正确的努力方向。