1.12 编程世界的那把锁
沿共享变量、互斥锁临界区、可见性与信号量许可追踪并发访问顺序,用故障实验定位等待与释放缺口。
学习目标
- 能沿请求进入、获取许可、修改共享态、发布可见性和释放许可追踪同步合同
- 能区分互斥锁保护临界区与信号量约束并发容量,并说明先行发生关系如何传递可见性
- 能在丢锁、许可泄漏、死锁和容量边界场景中定位首个偏离并从干净状态重放
1.12 编程世界的那把锁
本页依据刘欣《码农翻身》(2018 年第 1 版)及出版社公开书目信息,独立重构 1.12 编程世界的那把锁。正文、代码、图示、实验和练习都是本课程重新设计的教学材料,不复制原书正文、插图、练习答案或代码。
共享变量的问题不只是“两个线程同时写”。真正需要验收的是临界区的原子边界、获取与释放顺序、共享数据的可见性、等待关系和同步原语的容量。互斥锁通常保护一个互斥临界区,信号量用许可数限制同时进入者;两者都需要异常路径和所有权合同。
三个会让同步模型失真的陷阱
同步合同
↡本页把故事重构为由互斥锁、信号量、临界区和先行发生关系共同保护共享状态的并发同步模型。不是把锁拟人化,而是要求每次等待、获取、修改、发布和释放都可观察、可配对、可恢复。
信号量许可可以写成:
不变量是 0 <= permits <= capacity。互斥锁还要满足同一时刻最多一个所有者;共享状态的读取和写回要落在临界区或明确的原子协议内。最终结果正确,不足以证明中途没有越过临界区或泄漏许可。
五个目录节点到机制证据
1.12 编程世界的那把锁
↡由互斥锁、信号量、临界区和先行发生关系共同保护共享状态的并发同步模型。提供整条验收边界:固定共享不变量、锁或许可的容量、线程角色、异常路径和复位台账。
共享变量惹的祸
↡多个线程读写同一状态而没有足够原子边界、所有权或可见性协议时产生的竞态与不一致。要先把读、改、写和版本变化列成事件。只有最后数字相同,不能证明每次更新都被保留。
争抢吧,线程
↡多个线程竞争同一锁、信号量或资源时,按照等待、获取、占用和释放顺序形成的调度关系。要记录等待者、所有者、队列顺序和唤醒条件;依赖闭环是死锁入口,长期得不到许可则要检查饥饿与容量。
改进
↡通过缩小临界区、成对清理、原子发布、固定锁顺序或调整许可容量修复并发不变量的工程动作。不能只让失败概率变低。必须保存修复前后的首差、锁/许可轨迹和从干净状态重放结果。 还要说明修复改变了哪条同步合同,以及它带来的等待、吞吐或复杂度代价。
信号量
↡用计数许可表示可用容量,通过 acquire 消耗许可、release 归还许可并协调并发进入者的同步原语。的数值是资源预算,不等同于互斥锁所有权。每一次 acquire 都应有对应 release 或明确的所有权转移,许可范围不能越界。
最小可重放实现
semaphore = baseline(capacity=2)
acquire(semaphore)
with mutex:
shared.value = shared.value + 1
publish(shared.value)
release(semaphore)
assert 0 <= semaphore.permits <= semaphore.capacity
assert reset() == baseline(capacity=2)这段草图只表达同步合同,不复制书中叙事或代码。实际复核应保存线程、锁所有者、许可数、共享版本、临界区、发布点、异常清理和复位结果。
五步复核同步生命周期
1. 固定共享状态与资源容量
记录共享变量、初始版本、互斥锁、信号量容量、线程角色和不变量。先预测每个线程能够进入的次数与最终许可数。
Lab
锁、许可与异常清理实验
只改变一个竞争或异常条件,观察共享版本、等待图和许可不变量。
T1 获取锁并修改,T2 随后读取新版本
T1 lock → write v1 → unlock; T2 lock → read v1 → unlock
判定
通过:所有者、发布和释放顺序闭合
当前场景:基线同步;记录线程、锁所有者、共享版本、许可数、等待图、清理与复位。
正常、边界与故障证据
| 样本 | 只改变的变量 | 预期判定 | 必存证据 |
|---|---|---|---|
| 正常 | 锁配对、许可容量和临界区完整 | 共享版本推进,许可回到容量 | 所有者、版本、acquire/release 和提交 |
| 边界 | 许可为零、临界区变长或等待者接近上限 | 阻塞或排队,不越过容量 | 容量、队列、等待者、唤醒条件 |
| 故障 | 一次丢锁、许可泄漏或锁顺序反转 | 首个依赖/不变量违约可定位 | 首差、持有者、许可账、清理和复位 |
故障诊断:先找不变量失守的事件
- 核对资源账:比较锁所有者、信号量容量、acquire/release 次数和线程终态,找第一处负许可或未配对操作。
- 核对共享版本:排列读取、修改、发布和提交,确认所有写回都在临界区或明确原子协议内。
- 核对等待图:记录线程等待的资源和资源持有者;闭环是死锁入口,长期无唤醒则检查饥饿与丢失通知。
- 核对异常清理:对每个提前返回、异常、取消和超时路径验证解锁、release、所有权转移和复位。
术语表
名词解释
本章出现的专业名词,用大白话再讲一遍。
- 1.12 编程世界的那把锁
由互斥锁、信号量、临界区和先行发生关系共同保护共享状态的并发同步模型。
- 共享变量惹的祸
多线程读写同一状态而缺少原子边界、所有权或可见性协议时产生的竞态。
- 争抢吧,线程
多线程竞争锁、信号量或资源时形成的等待、获取、占用和释放关系。
- 改进
通过临界区、清理、发布、锁顺序或许可容量修复并发不变量的动作。
- 信号量
用计数许可表示容量,通过 acquire 消耗、release 归还的同步原语。
练习
练习
问题 1: 两个线程同时给共享计数器加一,最后只增加一次,最先要保存什么?
问题 2: 信号量容量为 2,三个线程都调用 acquire,第三个线程应该发生什么?
问题 3: 线程在持锁时异常退出,怎样避免后续线程永久等待?
本页小结
1.12 编程世界的那把锁的关键不是记住锁的比喻,而是能说明共享状态的原子边界、线程等待关系、许可容量、可见性和异常清理。完成标准是从请求进入重放到释放许可,在竞态、死锁或泄漏中定位首个不变量违约,并证明复位后锁、许可和共享版本重新闭合。