1.12 编程世界的那把锁

沿共享变量、互斥锁临界区、可见性与信号量许可追踪并发访问顺序,用故障实验定位等待与释放缺口。

学习目标

  • 能沿请求进入、获取许可、修改共享态、发布可见性和释放许可追踪同步合同
  • 能区分互斥锁保护临界区与信号量约束并发容量,并说明先行发生关系如何传递可见性
  • 能在丢锁、许可泄漏、死锁和容量边界场景中定位首个偏离并从干净状态重放

1.12 编程世界的那把锁

本页依据刘欣《码农翻身》(2018 年第 1 版)及出版社公开书目信息,独立重构 1.12 编程世界的那把锁。正文、代码、图示、实验和练习都是本课程重新设计的教学材料,不复制原书正文、插图、练习答案或代码。

共享变量的问题不只是“两个线程同时写”。真正需要验收的是临界区的原子边界、获取与释放顺序、共享数据的可见性、等待关系和同步原语的容量。互斥锁通常保护一个互斥临界区,信号量用许可数限制同时进入者;两者都需要异常路径和所有权合同。

三个会让同步模型失真的陷阱

同步合同

不是把锁拟人化,而是要求每次等待、获取、修改、发布和释放都可观察、可配对、可恢复。

信号量许可可以写成:

permitsafter=permitsbeforeacquire+releasepermits_{after}=permits_{before}-acquire+release

不变量是 0 <= permits <= capacity。互斥锁还要满足同一时刻最多一个所有者;共享状态的读取和写回要落在临界区或明确的原子协议内。最终结果正确,不足以证明中途没有越过临界区或泄漏许可。

同步合同:进入、修改、发布和释放必须成对可追踪锁保护互斥临界区,信号量保护容量,不变量贯穿异常路径1请求进入线程 + 资源顺序证据2获取许可lock / sem顺序证据3修改共享态临界区不变量边界4发布可见性版本 + 顺序顺序证据5释放许可唤醒 + 回收回收证据最终值正确不能覆盖中途竞态、死锁、可见性或许可泄漏
专属图示:把同步原语的顺序、容量和异常回收放进同一条合同。

五个目录节点到机制证据

1.12 编程世界的那把锁

提供整条验收边界:固定共享不变量、锁或许可的容量、线程角色、异常路径和复位台账。

共享变量惹的祸

要先把读、改、写和版本变化列成事件。只有最后数字相同,不能证明每次更新都被保留。

争抢吧,线程

要记录等待者、所有者、队列顺序和唤醒条件;依赖闭环是死锁入口,长期得不到许可则要检查饥饿与容量。

改进

不能只让失败概率变低。必须保存修复前后的首差、锁/许可轨迹和从干净状态重放结果。 还要说明修复改变了哪条同步合同,以及它带来的等待、吞吐或复杂度代价。

信号量

的数值是资源预算,不等同于互斥锁所有权。每一次 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 / 5

1. 固定共享状态与资源容量

记录共享变量、初始版本、互斥锁、信号量容量、线程角色和不变量。先预测每个线程能够进入的次数与最终许可数。

同步合同:进入、修改、发布和释放必须成对可追踪锁保护互斥临界区,信号量保护容量,不变量贯穿异常路径1请求进入线程 + 资源顺序证据2获取许可lock / sem顺序证据3修改共享态临界区不变量边界4发布可见性版本 + 顺序顺序证据5释放许可唤醒 + 回收回收证据最终值正确不能覆盖中途竞态、死锁、可见性或许可泄漏
专属图示:把同步原语的顺序、容量和异常回收放进同一条合同。

Lab

锁、许可与异常清理实验

只改变一个竞争或异常条件,观察共享版本、等待图和许可不变量。

T1 获取锁并修改,T2 随后读取新版本

T1 lock → write v1 → unlock; T2 lock → read v1 → unlock

判定

通过:所有者、发布和释放顺序闭合

当前场景:基线同步;记录线程、锁所有者、共享版本、许可数、等待图、清理与复位。

正常、边界与故障证据

同步证据矩阵:首个不变量违约决定修复入口正常看顺序,边界看容量,故障看所有者与清理观察项正常边界故障共享态版本递增临界区长丢失更新一主一进等待死锁许可范围内为零泄漏发布可见延迟旧值所有者、版本、许可账、等待图和发布点共同解释同步结果
专属图示:共享状态、锁、容量和可见性必须分别验收。
样本只改变的变量预期判定必存证据
正常锁配对、许可容量和临界区完整共享版本推进,许可回到容量所有者、版本、acquire/release 和提交
边界许可为零、临界区变长或等待者接近上限阻塞或排队,不越过容量容量、队列、等待者、唤醒条件
故障一次丢锁、许可泄漏或锁顺序反转首个依赖/不变量违约可定位首差、持有者、许可账、清理和复位

故障诊断:先找不变量失守的事件

  1. 核对资源账:比较锁所有者、信号量容量、acquire/release 次数和线程终态,找第一处负许可或未配对操作。
  2. 核对共享版本:排列读取、修改、发布和提交,确认所有写回都在临界区或明确原子协议内。
  3. 核对等待图:记录线程等待的资源和资源持有者;闭环是死锁入口,长期无唤醒则检查饥饿与丢失通知。
  4. 核对异常清理:对每个提前返回、异常、取消和超时路径验证解锁、release、所有权转移和复位。

术语表

名词解释

本章出现的专业名词,用大白话再讲一遍。

1.12 编程世界的那把锁

由互斥锁、信号量、临界区和先行发生关系共同保护共享状态的并发同步模型。

共享变量惹的祸

多线程读写同一状态而缺少原子边界、所有权或可见性协议时产生的竞态。

争抢吧,线程

多线程竞争锁、信号量或资源时形成的等待、获取、占用和释放关系。

改进

通过临界区、清理、发布、锁顺序或许可容量修复并发不变量的动作。

信号量

用计数许可表示容量,通过 acquire 消耗、release 归还的同步原语。

练习

练习

问题 1: 两个线程同时给共享计数器加一,最后只增加一次,最先要保存什么?

问题 2: 信号量容量为 2,三个线程都调用 acquire,第三个线程应该发生什么?

问题 3: 线程在持锁时异常退出,怎样避免后续线程永久等待?

资料与写作方式声明

本章以码农翻身权威目录界定学习范围,并结合正文列出的技术资料独立重写;不宣称复现原书正文,也不沿用原作表述。

原作版权归作者与出版社所有;本站原创教学结构与表述仅供学习交流。

本页小结

1.12 编程世界的那把锁的关键不是记住锁的比喻,而是能说明共享状态的原子边界、线程等待关系、许可容量、可见性和异常清理。完成标准是从请求进入重放到释放许可,在竞态、死锁或泄漏中定位首个不变量违约,并证明复位后锁、许可和共享版本重新闭合。

讨论

评论区加载中…