信号量

形式陈述 ​

信号量是带非负整数状态 $S\in \mathbb{N}$ 的同步对象。其两个基本原子操作公理库原子操作Atomic operation对并发观察者不可分割、可视为在单一瞬间完成的操作。通常记为 $P/V$、wait/signal 或 down/up：

$$\begin{array}{rl}P& :S>0\text{ 时令 }S\leftarrow S-1\text{ 并返回；否则调用等待},\\ V& :S\leftarrow S+1\text{，并可使一个等待调用重新具备完成条件}.\end{array}$$

抽象语义始终让 $S\ge 0$。某些实现内部用负计数编码等待者数量，但那是表示技巧，不应改写对象对外的许可语义。现代阻塞实现通常还维护等待队列：P 在没有许可时把调用者挂起，V 发布许可并让某个等待者重新参与调度；究竟选择哪个等待者、何时运行以及是否 FIFO，不属于基本定义。

初值 $C>1$ 的 counting semaphore 表示至多 $C$ 个可同时占用的许可。若每次 V 都只归还先前成功 P 获得的许可，则持有数 $H$ 与可用数满足 $H+S=C$，从而 $H\le C$。binary semaphore 把可用许可限制在 $0$ 或 $1$，可产生互斥效果；但它通常没有互斥锁公理库互斥锁Mutex · Mutex lock · 互斥量以所有权和阻塞语义封装临界区互斥的同步对象。的线程所有权约束，V 可以由与先前 P 不同的线程执行。

初值为零时，信号量还可表达事件交接：消费者的 P 在事件发生前等待，生产者执行 V 后留下一个可消费的许可。这里通知具有可计数状态；没有等待者时执行的 V 不会凭空消失，而是使后来的一个 P 直接完成。这一点与条件变量公理库条件变量Condition variable · Condition variable synchronization让线程原子地释放互斥锁并等待共享谓词可能变真的条件同步对象。的通知语义根本不同。

信号量只给出许可计数的安全规则。无饥饿、有界等待、优先级策略以及被唤醒者最终得到 CPU 都需要额外的实现和调度假设。线程获取许可后崩溃也可能永久减少可用容量，除非系统另有租约、失主检测或恢复协议。

直觉 ​

把 $S$ 看作柜台里尚未借出的令牌。P 必须拿走一枚令牌才能继续，没有令牌便等待；V 放回一枚。令牌会保存下来，所以它既能限制“同时有多少人使用资源”，也能记住“发生了多少次可消费事件”。信号量不关心谁归还令牌，这种弱所有权正是它比 mutex 更适合跨线程交接的原因。

计数把资源容量从互斥的“一次一个”推广为“一次至多 $C$ 个”，但它不会替应用维护资源本身。连接是否健康、许可是否与真实连接一一对应、异常路径是否归还许可，仍是调用者的责任；计数正确只能保证容量账本没有超发。

例子与边界 ​

一个数据库连接池有 $C=8$ 条连接。任务在取连接前执行 P(pool_slots)，成功后才从池中移出一条连接；使用完毕先把连接放回，再执行 V(pool_slots)。只要每次成功获取恰好对应一次释放，任意时刻最多八个任务持有连接。若异常路径漏掉 V，许可逐渐耗尽，最终所有新任务阻塞；这是资源泄漏造成的活性失败，不是信号量违反容量不变量。

另设初值为零的 ready。加载线程完成初始化后执行一次 V(ready)，等待线程执行 P(ready) 后继续。若 V 先发生，许可保存在 $S=1$ 中，后来到达的等待者仍能通过。不过一次 V 只供应一次 P；若所有未来线程都应观察一个永久成立的“已初始化”状态，持久布尔谓词或一次性初始化原语比不断补发许可更符合规格。

binary semaphore 虽能保护临界区，却允许线程 A 执行 P、线程 B 执行 V。把需要所有者一致性或优先级继承的 mutex 机械替换为它，会失去接口保证。反过来，若一个线程产生工作、另一个线程消费工作，跨线程 V/P 正是合法通信，强行套用所有者规则反而表达不了交接。

推论与应用 ​

信号量是有界缓冲区与生产者—消费者协议的经典构件：一个计数空槽，一个计数已填项目，再用互斥保护缓冲区结构。三个同步对象各管一个重心——许可计数描述容量，mutex 描述所有权互斥，条件变量描述受锁谓词的等待；把它们都叫作“通知机制”会掩盖不同的不变量。

正确性证明应把计数守恒、共享容器不变量与活性分开。前两者通常是安全性质；等待者最终得到许可则取决于生产者是否继续 V、实现如何选择等待者以及调度是否满足公平性公理库饥饿与公平性Starvation and fairness · 调度公平性 · 无饥饿用调度与服务选择的公平假设刻画持续请求者是否可能永久得不到完成机会。。测试中看到所有线程都运行过，不能替代这一量词明确的进展论证。

参考资料

• E. W. Dijkstra, “Cooperating Sequential Processes,” 1965；以及 THE multiprogramming system 的同步设计。
• The Open Group, POSIX Semaphores, sem_wait 与 sem_post 规范。
• Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012。