互斥

互斥是临界区占用数至多一的不变量，而“有人最终能进去”“每个等待者最终能进去”分别是更强的活性与公平条件。把这些性质拆开，可以看清一个算法是因冲突规则错误破坏安全，还是因调度、崩溃或服务顺序失去进展。互斥锁公理库互斥锁Mutex · Mutex lock · 互斥量以所有权和阻塞语义封装临界区互斥的同步对象。是带获取、释放与所有权的同步对象；互斥规格也可由消息令牌或其他原子对象实现，二者不能互作同义词。

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

具体锁实现的边界由自旋锁公理库自旋锁Spinlock · Spin lock获取失败时以原子操作持续轮询、等待锁在短时间内释放的互斥锁实现族。页承接：TAS 依赖原子读改写，ticket lock 增加请求顺序，却仍受抢占、缓存争用和调度假设影响。持锁线程停止时互斥安全性仍可成立，而阻塞、死锁与恢复属于锁对象及执行模型的进展分析。

互斥本身是一条安全性与活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。中的安全性质：任何时刻至多一个进程在临界区。无死锁、无饥饿和有限等待属于不同强度的活性条件。

把计数信号量公理库信号量Semaphore · Counting semaphore · 信号灯以非负计数保存可用许可，并用原子等待与释放操作协调容量或事件的同步原语。初始化为一，并令 P/wait 与 V/signal 原子化，可以实现临界区入口的互斥：成功减到零的线程进入，其余线程等待，退出时再释放。该实现只给出容量约束；公平唤醒、优先级反转、进程崩溃后的许可恢复和可重入性仍需额外协议。

共享内存系统公理库共享内存系统Shared-memory system进程通过读写共享对象交互的并发模型。可用原子操作公理库原子操作Atomic operation对并发观察者不可分割、可视为在单一瞬间完成的操作。维护互斥不变量，读改写原语公理库读改写原语Read-modify-write operation · RMW在单个原子步骤中读取旧值、计算并写入新值的共享内存操作。则实现具体锁入口。阻塞 mutex公理库互斥锁Mutex · Mutex lock · 互斥量以所有权和阻塞语义封装临界区互斥的同步对象。与忙等锁公理库自旋锁Spinlock · Spin lock获取失败时以原子操作持续轮询、等待锁在短时间内释放的互斥锁实现族。共享互斥目标，却采用不同等待策略；死锁公理库死锁Deadlock · 资源死锁一组参与者因等待依赖闭合而彼此无法再完成所需动作的全局进展失败。和饥饿/公平公理库饥饿与公平性Starvation and fairness · 调度公平性 · 无饥饿用调度与服务选择的公平假设刻画持续请求者是否可能永久得不到完成机会。再分别刻画全局等待闭环与个体服务保证。

数据库和操作系统还需把互斥与优先级反转、故障恢复及临界区粒度共同设计。这些工程约束不改变“临界区至多一人”的核心公式，却决定实现能否持续提供服务。