形式陈述

设每个进程循环经过 remainder、entry、critical 与 exit 区。互斥的安全条件是

$$ \forall\text{ reachable states},\qquad \#\{i:i\text{ 位于 critical section}\}\le1. $$$$\mathrm{\forall }\text{ reachable states},\mathrm{\#}\{i:i\text{ 位于 critical section}\}\le 1.$$

完整互斥问题通常另要求进展性质，例如无死锁、无饥饿或有界等待；这些并不蕴含于上式。

直觉

互斥只说临界区不能同时有两人进入。一个把所有进程永远挡在门外的算法满足互斥，却完全没有用，因此安全与进入进展必须分开陈述和证明。

例子与边界

单个布尔变量 busy 上的“先读 false，再写 true”若读写之间非原子，两个线程可同时通过，违反互斥。Peterson 两进程算法在顺序一致且读写原子的模型下兼顾互斥与进展，但不能不加说明地移植到弱内存或任意数量进程。

推论与应用

互斥用于保护非线程安全状态和实现锁。证明通常寻找“两个进程同时在临界区”会导致矛盾的不变量；性能还需评估等待、争用、公平性与故障情况下的阻塞。

参考资料

• Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012，Chs. 2, 7。
• Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004，Chs. 4–5。