跳转到内容
← 返回计算理论
计算理论当代约 20 分钟阅读

Knuth 1966:互斥的集体进展怎样仍允许一个人被永远超过

Additional Comments on a Problem in Concurrent Programming Control

Knuth互斥饥饿CACM 1966

1966 年 5 月,唐纳德·厄尔·克努斯(Donald E. Knuth)在 Communications of the ACM 第 9 卷第 5 期发表《Additional Comments on a Problem in Concurrent Programming Control》,页码 321,排到 322 上栏,体裁是半页评论。DOI 为 10.1145/355592.365595。作者单位印作加州理工学院(California Institute of Technology)。对象是一份已发表的短评:Dijkstra 1965 那一页已经给出 \(N\) 台计算机、只用共享整型与布尔、没有中央仲裁者的临界区互斥;克努斯构造一种调度,使一台一直想进的计算机看着别人反复完成临界区,互斥作为安全性可以仍成立,个体活性则失败。他同时点名哈里斯·海曼(Harris Hyman)1966 年 1 月那则两人「简化」(CACM 9(1),页码 45;克努斯原文把期次误写成 Jan. 1965,第 9 卷实为 1966 年)几乎完全不能用:两台可以同时进入临界区。评论后半给出自己的 \(N\) 机构造,并把个体等待收成有上界的句子:别人至多再进入 \(2^{N-1}-1\) 次。封面停在这一刀量词,不把公平写成先来先服务。

它不是 唐纳德·克努斯 的人物页,不是《计算机程序设计艺术》,不是大 \(O\)、不是 TeX,也不是文学编程。它不是 艾兹格·迪科斯彻 的人物页,不是 1968 年「goto 有害」,不是 THE 操作系统,不是信号量,更不是银行家算法。它不是 Dijkstra 1965 本身:那一页是问题—解—证明的封面;本页是八个月后钉在条件 (d) 上的评论。它更不是 兰波特 1974 年的面包店算法。面包店用门口与号码把「先请求」收成可比较的先后;本页还没有票根,有界等待不等于先来先服务。后来把两进程写成两面旗加一个 \(TURN\) 的短注,见 Peterson 1981。它不是 并发 总览,不是 等待自由,不是线程库或锁省略,也不是布置、绕过或让互斥失效的操作单。德克尔的两进程解、海曼的两人稿、德布鲁因 1967 与艾森伯格、麦圭尔 1972 的后续评论,都是邻居,不是本页转载的正文。

破除误解:饿死不是死锁,有界等待也不是先来先服务

第一层误解把本页听成《计算机程序设计艺术》里某一章并发,或听成克努斯凭空发明了互斥。1965 年 9 月那一页已经把 \(N\) 机互斥写成可推理的问题;克努斯 1966 年 5 月要钉的,是那一页条件 (d) 实际写下的量词。人物页上的 MIX、断行与支票轶事属于另一条生涯,封面不是这一半页。把短评收成「算法分析名家顺便写了锁」,会把对象从「集体进展允许无限超过」换成名人录。

第二层误解把迪科斯彻的条件 (d) 听成「每一个想进的人终将进入」,或把饿死听成死锁。1965 年要排除的是:临界区空着、又有人在入口打转时,不能为他们安排有限速度,使「谁先进入」被拖到永恒。那是关于集体的进展:不会全体永远进不去。它不担保某一个编号不会被别人无限次超过。死锁是全体卡住、临界区一直空着;饿死是别人仍在进出,唯独某台永远排在外面。克努斯写明:迪科斯彻的算法保证不会全体同时被堵住,却仍可能让个体等到永恒。他补了一句语境:迪科斯彻在问题陈述里决定允许这种可能,因为他关心的是临界区平均需求较低的情形;可是确有许多应用不能接受个体被堵住。把 (d) 读成公平,会把一页里实际写下的量词撑大;把本页读成「1965 年的解会死锁」,则把两种活性故障焊成一个词。

第三层误解把克努斯自己的构造听成 面包店 的预习,或听成先来先服务已经在 1966 年写完。本页离开临界区时,把整数 \(k\) 交给循环编号上的前一位,再用三取值的控制字做两道门。等待被收成上界:一台在入口打转时,别人至多再完成 \(2^{N-1}-1\) 次临界区。\(N=4\) 时这个数字是 7。有界意味着个体不会被无限超过,并不意味着先走出某段无循环门口的人一定比后来者更早进入。先来先服务要到 1974 年才被写成合同第 2 款,而且假设更弱:重叠读可以返回任意值。德布鲁因 1967 年把上界收到 \(\frac12 N(N-1)\);艾森伯格与麦圭尔 1972 年再收到 \(N-1\)。那些后文仍围着共享控制变量打转,是邻居。把半页听成票号算法,或听成「公平问题到此闭合」,年份与量词都错了。

第四层误解把标题听成生产环境的同步手册,或听成海曼那则两人稿可以当课堂配方。海曼声称简化了两人情形;克努斯指出两台可以同时把 \(k\) 写成自己并一起进入临界区,「简化」几乎完全不能用。本页复述 1965 年标号与自己的控制字,是为了让调度与上界能被跟上,不是一份把赋值抄进线程库的清单。读写一个字仍被当成不可分割;证明是操作叙事,不是模型检验脚本。把这一半页听成可上线的临界区模板,或听成教人如何让互斥失效、如何绕过入口的步骤,类型都错了。概念证据到此为止,不是配方。

1966 年的装置:一种调度,以及把等待收成指数上界

先钉 1965 年那一页实际担保的句子。\(N\) 台计算机共用一块存储器,每台跑循环,循环里有一截临界区。解必须对称、不靠相对速度、临界区外停机不得卡住别人,并且满足 (d):若不止一台即将进入,则不可能设计出有限速度,使「谁先进入」被推迟到永恒。公共存储是布尔数组 \(b,c[1:N]\) 和一个整数 \(k\)。第 \(i\) 台先把 \(b[i]\) 写成假,表示自己已离开可停机的剩余段。若当前 \(k\) 不是 \(i\),它把 \(c[i]\) 写成真,并在看见 \(b[k]\) 为真时把 \(k\) 改成 \(i\)。若 \(k\) 已经是 \(i\),它把 \(c[i]\) 写成假,再扫描其余的 \(c\);全部为真才进入临界区。证明的第二截说:没有人在临界区时,打转者里至少一台——因而恰好一台——将及时被允许进入。\(k\) 会在有限次赋值后冻结,指向某一个打转者。这句话排除全体谦让,没有排除「冻结永远轮不到某一号」。

克努斯给出的调度把这句缺口变成画面。时间不妨看成离散格子——他说这对许多计算机系统成立,对本例方便,却并非严格必要。假定一号计算机在迪科斯彻程序的标号 L13 处打转,时刻 \(0,10,20,30,\ldots\) 都停在那里,看见 \(b[k]\) 为假且 \(k\neq i\)。其余计算机完全可以在这些采样点之间改写 \(b[k]\) 并改 \(k\),使一号永远跳不出循环。一个具体安排:\(k=N=2\) 时,二号可以在时刻 \(10n+2\) 把 \(b[2]\) 写成真,再在 \(10n+9\) 回到 L20 把它写成假,对任意多个 \(n\) 重复。于是二号反复进入并离开临界区,一号一直想进,一直看见门关着。互斥没有破:任意时刻至多一台在里面。集体进展也没有破:总有人在进出。被打破的是未写出的那句全称——「每一个已经靠近入口的编号终将进入」。本页复述这些标号,是为了让反例能被核对,不是布置入口协议的步骤。

海曼那则两人稿被放在评论开头,当作另一种失败。它不是饿死,是安全性直接垮掉:两台可以同时认为自己拥有 \(k\),同时进入临界区。克努斯说他希望这封信能让人省掉误用那两种方法会碰到的麻烦。点名海曼是为了标明「缩短两人写法」并不自动继承 1965 年的合同;点名迪科斯彻是为了标明合同里那条活性从一开始就比后来文献所说的饥饿自由更弱。两刀切的是不同的句子,不要收成同一则勘误。

评论后半给出克努斯自己相信正确的构造。公共存储改成整数数组 \(\mathrm{control}[1:N]\) 和一个整数 \(k\)(初值为零)。控制字只取三档:不在尝试里、已声明想进、已抬到第二道门。扫描从当前 \(k\) 沿编号递减绕一圈;第二道门上若两人同时声称,则退回重来。离开临界区时把 \(k\) 交给循环上的前一位,偏好因此旋转,而不是 1965 年那种谁先改 \(k\) 谁被提名。克努斯说他试过十几套写法才得到自认为正确的一份。本页讲这些职务,是为了让上界论证能被跟上,不是一份可抄进线程库的清单。

上界被写成:一台在入口等待时,其余计算机至多再执行 \(2^{N-1}-1\) 次临界区。论证在原文里是一份情景提纲,不是从公理到定理的形式推演。\(N=4\) 时他请读者设想四号停在第一道门,一、二、三号已经在第二道门上。然后一号高速走完临界区;二号走完、一号又回到第二道门;一号再走完;三号走完、一号与二号依次回到第二道门;接着把前面三步再演一遍。七次进入发生时,四号一直不幸地错过那些短暂出现、本可以让它抬到第二道门的 \(k\) 值。七等于 \(2^{3}-1\)。指数来自这种「外圈的人走完一圈,内圈的人把偏好又抢回去」的嵌套,不是来自票号。后来文献把这份构造称为第一份饥饿自由的 \(N\) 进程互斥;那是回顾性的名字。1966 年写下的句子是等待有上界,以及「我相信这就正确」。若一台在入口协议中途停死,别人仍可能被堵住——这一点与 1965 年同类,本页没有声称故障隔离。

它证明了什么,没有覆盖什么

它证明了:Dijkstra 1965 的条件 (d) 是集体进展,不是个体饥饿自由;存在一种有限速度的交错,使互斥保持、别人反复进入,而某一台永远停在入口。它也给出一份克努斯自认为正确的 \(N\) 机构造,把个体等待收成 \(2^{N-1}-1\) 的上界,并把 1965 年两个布尔数组收成一个三取值控制字、把提名收成循环交接。意义首先是量词:并发里最容易被听错的,不是「有没有锁」,而是「不会全体卡住」与「每一个人都轮得到」不是同一句话。海曼的两人稿则从反面标明:缩短变量个数并不自动保住安全性。

它没有证明先来先服务。有界等待允许后来者在上界之内多次超过已经在打转的人;Lamport 1974 才把「先走完门口」焊到「更早进入」上,并且把存储器按台分开、允许重叠读返回任意值。它没有覆盖德布鲁因把上界收到二次、艾森伯格与麦圭尔收到 \(N-1\) 的那些后文;那些评论仍是邻居。它没有覆盖 Peterson 1981:两人、三枚变量、旗与 \(TURN\) 是十五年后的短注。它没有给出测试并设置,也没有把互斥收成操作系统里的一种系统调用。信号量、哲学家进餐与银行家算法属于 迪科斯彻 随后几年的另一条工作,封面不同。

它没有覆盖 等待自由:持有临界区或停在第二道门上的进程,按设计可以挡住别人;等待自由拒绝这种挡住。有界等待只在别人持续走完入口、临界区与出口时才兑现;别人停在里面,等待者仍然进不去。它没有覆盖线性化:临界区是一段程序文本,不是对象上带调用—返回区间的生效点。它没有覆盖弱内存模型下「先写控制字、再读别人的控制字」会不会一起看到旧值。它没有把归纳断言写到这些标号的边上,也没有给出模型检验脚本。本页不提供如何把上述赋值抄进线程库、如何布置锁省略、如何让互斥失效或绕过临界区的步骤。半页回答的是「集体进展怎样仍允许一个人被永远超过」;面包店回答的是「没有中央 \(k\)、读可以任意时,互斥能否带上先来先服务」。两句都不是操作单。

跨域连接

  • 证明:克努斯没有推翻 1965 年互斥那一句,他造了一个调度,使另一句未被写出的全称命题失败。数学里的反例必须对准被声称的量词:集体存在性的活性证明,挡不住个体全称的活性反例。本页后半的上界同样是操作叙事,\(N=4\) 的七次超过是情景提纲,结尾仍是「我相信」。证书类型与 1965 年那页一样尚未闭合;差别只在被检查的句子从「不会全体卡住」换成了「不会有人被无限超过」。
  • 认识论:看见别人反复完成临界区,并不能推出「我终将进入」。一号计算机在固定节拍上取样,每次都得到「门关着、\(k\) 不是我」;它无法从这些观察恢复二号在采样点之间写过真值的那段历史。条件 (b) 本来就禁止把相对速度当成公共知识;克努斯的调度把这条禁令收成认识论上的陷阱:你合法拥有的只有自己读到的字,而调度者可以安排这些字永远不显示「现在轮到你」。
  • 自由:对称性禁止把某台写成永久的末位;循环交接进一步禁止「同一提名永远压在某一号头上」。可是互斥本身又是一种严格的消极自由:当我处于临界区,别人进入的自由被暂停。1965 年保护的是「不得全体失去进入的可能」;本页追问的是「不得在我想进时被无限超过」。前者是集体的免于停滞,后者是个体的免于被永远插队。两句都不是等待自由意义上的不受阻挡:停在临界区里的人,仍然按设计暂停他人。
  • 等待自由:1991 年的尺从反面量这篇。等待自由要求我完成自己的操作只靠自己的有限步,哪怕别人已经停机。临界区按定义把别人的进入交给我何时离开;若我停在里面,等待者永远进不去。克努斯的 \(2^{N-1}-1\) 只在别人持续走完协议时才是上界;它把「无限次超过」改成「有限次超过」,没有把挡住改成不挡住。赫利希后来证明:只用寄存器,两个进程甚至无法等待自由地达成共识。1966 年能做成的,恰好是一种必须阻塞、却把阻塞次数封顶的协调。
  • 正义:把临界区当成一种稀缺位置,集体进展相当于「只要还有人排队,窗口就不能永久关门」;个体饥饿自由相当于「已经排队的人不能被后来者无限插队」。先来先服务更强:后来者根本不该插到先走完门口的人前面。三种标准都像公平,量词却一层比一层紧。克努斯的贡献是把第二层从第一层里拆出来,并给出一份他相信满足第二层的装置;第三层要到面包店才成为封面。制度设计里若只检查「系统没有停摆」,就会漏掉那个永远被超过的人。

参考文献

  • Donald E. Knuth, "Additional Comments on a Problem in Concurrent Programming Control", Communications of the ACM 9(5), 1966, pp. 321–322. DOI: 10.1145/355592.365595. —— 本文对象:针对 Dijkstra 1965 条件 (d) 的饥饿调度,以及带 \(2^{N-1}-1\) 等待上界的 \(N\) 机构造。
  • E. W. Dijkstra, "Solution of a Problem in Concurrent Programming Control", Communications of the ACM 8(9), 1965, p. 569. DOI: 10.1145/365559.365617. —— 原问题、共享变量解与集体进展条件 (d);本页要钉的封面。
  • Harris Hyman, "Comments on a Problem in Concurrent Programming Control", Communications of the ACM 9(1), 1966, p. 45. DOI: 10.1145/365153.365167. —— 本页开篇点名的两人「简化」;克努斯指出其安全性失败。
  • N. G. de Bruijn, "Additional Comments on a Problem in Concurrent Programming Control", Communications of the ACM 10(3), 1967, pp. 137–138. DOI: 10.1145/363162.363167. —— 把等待上界收到 \(\frac12 N(N-1)\) 的后续评论,邻居不是封面。
  • M. A. Eisenberg and M. R. McGuire, "Further Comments on Dijkstra's Concurrent Programming Control Problem", Communications of the ACM 15(11), 1972, p. 999. DOI: 10.1145/355606.361895. —— 再把上界收到 \(N-1\);仍属围着共享控制变量打转的邻居。
  • Leslie Lamport, "A New Solution of Dijkstra's Concurrent Programming Problem", Communications of the ACM 17(8), 1974, pp. 453–455. DOI: 10.1145/361082.361093. —— 门口与号码上的先来先服务;本页对照的后文,不是补丁。
  • G. L. Peterson, "Myths About the Mutual Exclusion Problem", Information Processing Letters 12(3), 1981, pp. 115–116. DOI: 10.1016/0020-0190(81)90106-7. —— 两进程旗与 \(TURN\),用以标明人数、变量与年份都不是本页。
  • Maurice Herlihy, "Wait-Free Synchronization", ACM Transactions on Programming Languages and Systems 13(1), 1991, pp. 124–149. DOI: 10.1145/114005.102808. —— 等待自由与共识数,用以标明有界等待的互斥仍落在该尺的反面。

延伸阅读

  • 与 Dijkstra 1965 对读:先看那一页实际写下的四条禁令,再看本页把 (d) 的量词拆开。
  • 与 Lamport 1974 对读:有界等待允许上界之内的超过;先来先服务把超过从合同里删掉,并拆掉中央 \(k\)。
  • 与 唐纳德·克努斯 对读:人物页上的 TAOCP 与 TeX 都不是这一半页;先看互斥评论,再看算法分析那条生涯。
  • 与 Peterson 1981 对读:两人短注要解决的是「简单的正确解是否只能是德克尔」,不是饥饿上界。
  • 与 并发 对读:总览里的锁与死锁是教学装置;本页问的是死锁自由与饥饿自由怎样被写成不同的句子。
  • 与 等待自由 对读:把超过次数封顶,仍把进展交给别人是否离开临界区。