Peterson 1981：两进程互斥怎样用两面旗与一个 turn 写成短注

破除误解：简单不是唯一属于德克尔，证明也不必先变成厚册#

第一层误解把两进程互斥听成「德克尔已经是唯一简单的正确解」，或听成正确写法必须绕成套环。彼得森开篇点名同一期刊里多兰与托马斯（R. W. Doran 与 L. K. Thomas）1980 年那篇变体：他们给出的是德克尔型解的部分简化，去掉了先前发表稿里「环里再套环」的骨架，但仍被写成德克尔家族的修修补补。彼得森说，德克尔的原解由 迪科斯彻 在《协作的顺序进程》里详细讨论；后来的许多改写里，他点名霍尔特、格雷厄姆、拉佐夫斯卡与斯科特 1978 年的教材或许最好——随即加了一句：可惜作者们把自己正确的解当成了错的。本页给出的入口只有一次举起旗、一次写下 \(TURN\)、一处等待；出口只把旗放倒。结构一旦短下来，证明也可以短下来。把「正确」与「复杂」焊死，正是短注要拆的那句神话。

第二层误解把「可推导」听成神秘灵感，或反过来听成必须先有一套庞大的形式体系才能动手。短注明确写：这套协议并非凭空掉下来，而是两个更原始、各自会死锁的装置的并。第一件只靠 \(TURN\) 轮流：谁写下自己的编号，就等到编号变成对方的；它在对方不再循环尝试时会死锁。第二件只靠旗：举起自己的旗，等到对方的旗为假；它在两人都想进时会死锁。两种等待故障不相交，正确解是把两件叠在同一条入口上。神话里的「推导极难」，在这里被收成一句组合。迪科斯彻随后为这套协议写过一份断言证明（EWD 779，1981 年，伯勒斯公司油印）；彼得森在注里说，对如此简单的算法，那份证明在他看来不自然地复杂。把本页听成「必须先读完弗洛伊德式边上断言才算懂」，或听成「口语证明不算证明」，都会把短注自己选择的证书类型换掉。弗洛伊德 1967 是另一种几何；本页用的是关于谁被卡住、\(TURN\) 最后一次写向谁的操作论证。

第三层误解把德克尔听成可以原样改几个下标就变成 \(N\) 人，或把本注图 3 听成本页的主对象。彼得森另写了一则神话：德克尔的解并不能平凡改成 \(n\) 进程。据他所见，已知算法往往要大改形态，结果变成全新算法，哪怕 \(n\) 就是 2。同注确实附了一张把两进程协议重复使用 \(n-1\) 层、每层至少淘汰一人的草图，说明其来源是 L. 赫列恰尼克（L. Hrechanyk）的三进程解，正确性「留给读者」，并立刻声明它要用 \(2n-1\) 个取值到 \(n\) 的共享变量，而已知有变量少得多、约束更强的算法。这张草图属于这两页纸的附录动作，不是本页要停住的合同。后来文献里把彼得森扩成锦标赛或过滤器的那些 \(N\) 人写法，是后文，不是 1981 年 6 月这一则短注。把两人解直接复制 \(N\) 份，并不自动满足 1965 年那一页写下的四条禁令；那一页与这一则人数、变量、封面都不同。

第四层误解把标题听成课堂互斥操练、pthreads 配方，或听成已经给出现代弱内存模型下的可移植写法。短注假定的往来仍是对共享变量的赋值与对布尔公式的重复观察；公式不被原子求值，意味着「看见对方旗为假」与「看见 \(TURN\) 对自己有利」可以分两次读到，中间别人可以插进来。安全性论证依赖的是：若两人几乎同时做完等待里的测试，\(TURN\) 只能对其中一人有利；若一人先通过，另一人在通过前必须再做赋值，而测试前最后一次赋值会把 \(TURN\) 写成对自己不利的值，测试注定失败。这种讲述把「先写 \(TURN\)、再读旗与 \(TURN\)」当成可比较的先后。顺序一致性 两年前才被写成多处理器合同；弱模型上两面旗与一个 \(TURN\) 可以同时看见对方的旧值，朴素的先写后读会一起进入临界区。本页不把屏障、锁前缀或缓存协议写进 1981 年。把这两页听成可上线的临界区模板，或听成教人如何让互斥失效、如何绕过入口的步骤，类型都错了。概念证据到此为止，不是配方。

1981 年的装置：两面旗、一个 TURN，以及把两种死锁拆开再叠回去#

问题从两个异步进程说起。要找的是入口协议与出口协议。互斥是两人不得同时处于临界区。活性在本注里写成：不得死锁、不得锁死，亦即没有人在协议里永远等下去。更形式的定义，作者指向自己 1979 年罗切斯特大学技术报告《Concurrency and complexity》。通信手段就是那三枚共享变量。\(Q1\) 只由第一人赋成真或假，供第二人观察；\(Q2\) 对称。\(TURN\) 两人都会写。旗为真表示「我已声明要进」；\(TURN\) 记下最近一次把礼貌牌翻向自己的人——测试前最后一写对自己不利，因而把平局判给先写完的那一个。本页复述这些职务，是为了让两页里的证明能被跟上，不是一份把赋值抄进线程库的清单。

第一人的入口是：把 \(Q1\) 写成真，把 \(TURN\) 写成 1，然后等到 \(Q2\) 为假或者 \(TURN\) 等于 2。通过之后进入临界区。出口只把 \(Q_1\) 写回假。第二人对称：旗写成真，\(TURN\) 写成 2，等到对方旗为假或者 \(TURN\) 等于 1，离开时把旗放倒。等待是空循环直到布尔为真，不是嵌套的「先看旗再看轮次再撤回再重试」。与德克尔相比，少掉的正是那种在对方也要进时把自己的旗暂时放倒、把轮次让出去、再重新举起的退让骨架。彼得森不把退让写成单独一层控制；礼貌被收进「最后一次写 \(TURN\)」这一次赋值里。

锁死论证先固定第一人，假定他被按在那一处等待上永远出不去。有限时间之后，第二人只可能处于三类事情之一：根本没在尝试进入；卡在自己的入口协议里；或者一次次循环完成自己的协议。第一类，第一人会看见 \(Q_2\) 为假，于是通过。第二类不可能两人同时永远等：\(TURN\) 不是 1 就是 2，总有一人的等待条件已经成立。第三类，第二人会很快把 \(TURN\) 写成 2，并且不再写回 1，于是第一人通过。对称的句子对第二人同样成立。短注把「无人永远卡在协议里」写成这三类的穷尽，而不是写成关于相对速度的假设。

互斥论证用反证。若两人竟然同时处于临界区，则当时两面旗都为真。他们各自在进入前不久做完的那次测试，不可能「大约同时」都成功：\(TURN\) 只能对其中一人有利，另一半测试对两人都失败。于是必有一人先通过测试；第二人在通过之前还做了一次或多次赋值，并且是靠看见 \(TURN\) 对自己有利才通过的。可是测试前最后一次赋值把 \(TURN\) 写成了对自己不利的值，这次测试注定失败。互斥因此保住。论证短，依赖的是 \(TURN\) 的取值互斥，以及「最后一写」在观察者看来确实发生在测试之前。它没有按全部交错逐条展开，也没有把标签贴在流程图的边上。

它证明了什么，没有覆盖什么#

它证明了：两进程互斥不必绑在德克尔那种带撤回的套环上；存在一种只用两面旗与一个 \(TURN\)、入口只有一处等待的构造；该构造按作者的三类锁死论证与「最后一写对自己不利」的互斥论证，满足同时至多一人在临界区、且无人在协议里永远等待。意义首先是存在性与可理解性：并行算法未必那么难懂；复杂证明有时只是复杂骨架的影子。作者自己把「两进程互斥需要复杂解与复杂证明」写成被这两页结束的神话，并把「推导极难」写成被两个原始死锁装置的组合所拆穿的神话。

它没有把德克尔收成唯一前驱之外的全部历史，也没有重做 Dijkstra 1965 的 \(N\) 机合同。它没有覆盖克努斯 1966 年对 \(N\) 机个体饥饿的那半页：本注的锁死论证钉的是两人、三枚变量；把那半页拿来当本页封面，人数错了。它没有给出测试并设置、比较并交换，也没有把互斥收成操作系统里的一种系统调用。信号量、哲学家进餐与银行家算法属于 迪科斯彻 另一条工作，封面不同。同注图 3 的 \(n\) 层草图被作者自己降格为变量更多的示意，不是一份已闭合的 \(N\) 人证明；后来那些更省变量的 \(N\) 人推广是后文。

它没有覆盖 线性化：临界区是一段程序文本，不是对象上带调用—返回区间的生效点。它没有覆盖 等待自由：持有临界区的人按设计可以挡住别人；等待自由拒绝这种挡住。它没有覆盖 内存一致性模型 在弱序下哪些旗与 \(TURN\) 的搭配会失效。它没有把 归纳断言 写到这些赋值的边上，也没有把 EWD 779 收成自己的正文。本页不提供如何把上述赋值抄进 pthreads、如何布置锁省略、如何让互斥失效或绕过临界区的步骤。两页回答的是「两进程互斥是否必须复杂」；1965 年那一页回答的是「没有仲裁者时 \(N\) 机互斥能否被推理」。两句都不是操作单。

跨域连接#

• 证明：彼得森把短注收成「结构简单，所以证明也可以简单」，等于承认：并发控制的证书应当跟着骨架走，而不是先假定证书必须厚。可是这份证明仍是操作叙事：锁死靠三种去向穷尽，互斥靠 \(TURN\) 不能同时对两人有利，再加上「测试前最后一写对自己不利」。布尔公式不被原子求值，意味着测试本身不是一条不可分割的观察。结尾没有「作者相信这就完成了证明」那种自我保留，却把更形式的断言证明推给迪科斯彻并评为过重。数学里的证明要求量词写全；并发里最常见的事故，正是把「两人不会一起卡死」听成「任意人数、任意调度下每一个人都公平轮到」，或把口语论证听成已经在弱内存模型上闭包。
• 认识论：两面旗回答「他有没有声明要进」；\(TURN\) 回答「若两人都声明了，最近一次礼貌牌翻向谁」。短注禁止把尚未观察的相对速度提升为关于他人意图的知识：锁死论证里的三类去向，用的都是对方已经写下的旗与 \(TURN\)，而不是「我猜他已经放弃」。测试前最后一写必须对自己不利，是一份关于许可何种证据的合同：你不能既做完那次赋值，又声称自己同时看见了对自己有利的 \(TURN\)。把「我先到」当成不需要公共字就能成立的私有知识，正是互斥协议要拒绝的那类解。可理解性在这里也是认识论主张：若一套并行写法只能靠外人看不懂的证明来支撑，作者宁愿先怀疑写法本身。
• 等待自由：1991 年的尺从反面量这篇。等待自由要求我完成自己的操作只靠自己的有限步，哪怕别人已经停机。临界区按定义把别人的进入交给我何时离开；若我停在里面，等待者永远进不去。本注的无锁死保护的是「卡在入口协议里」的人，并不保护停在临界区里的人。赫利希后来证明：只用寄存器，两个进程甚至无法等待自由地达成共识。1981 年能做成的，恰好是一种必须阻塞的两人协调。把「彼得森已经把互斥变简单」听成「共享变量上一切进展条件都已解决」，会把短注的存在性证明误认成共识数表的底端。寄存器够写两进程互斥，不够写两人的等待自由共识——两句话可以同时真。
• 顺序一致性：1981 年的短注没有把多处理器合同命名。证明里用到的先后却常常跨过两枚变量：先写自己的旗与 \(TURN\)，再读对方的旗与 \(TURN\)。若机器允许这些步骤在另一进程看来颠倒，互斥那句「最后一写注定让测试失败」就不再能从装置里推出来。兰波特 1979 年把「看起来像某一条尊重程序序的交错」写成多处理器必须承认的外观，并证明单处理器各自顺序并不足够。本页的两面旗加一个 \(TURN\)，是那篇短注里先写后读反例的亲戚：跨单元的礼貌牌，正是弱可见性最先咬住的模式。1979 年命名的是让 1981 年这种讲述合法的条件，不是把这一则 IPL 改写成芯片手册。
• 自由：没有静态优先级，意味着谁都不得预先占有「先进入」的权利；\(TURN\) 只记录最近一次自我设障。可是互斥本身又是一种严格的消极自由：当我处于临界区，别人进入的自由被暂停。暂停有期限，前提是我终将离开并把旗放倒。短注用「不得在协议里永远等待」保护入口上的人，并不把「不得被静态排到末位」与「停在临界区里也不得挡住别人」写成同一句自由。去掉德克尔式的多层退让，并不自动得到等待自由意义上的不受阻挡。礼貌被写成一次对自己不利的赋值，而不是写成永久立法者。

参考文献#

• 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\) 的短注，以及关于复杂解与平凡推广的神话。
• E. W. Dijkstra, "Cooperating Sequential Processes", in F. Genuys (ed.), Programming Languages, Academic Press, 1968, pp. 43–112. —— 详细讨论德克尔的两进程解，被本注当作原解的出处；手稿为 EWD 123。
• 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. —— \(N\) 计算机共享变量互斥，用以标明本页人数与变量都不是这一页。
• R. W. Doran and L. K. Thomas, "Variants of the software solution to mutual exclusion", Information Processing Letters 10(4–5), 1980, pp. 206–208. DOI: 10.1016/0020-0190(80)90141-6. —— 本注开篇对照的德克尔型部分简化。
• E. W. Dijkstra, "An assertional proof of a program by G. L. Peterson", EWD 779, Burroughs Corporation, 1981. —— 本注称为对如此简单算法显得过重的断言证明。
• Leslie Lamport, "How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs", IEEE Transactions on Computers C-28(9), 1979, pp. 690–691. DOI: 10.1109/TC.1979.1675439. —— 顺序一致性，用以标明本页证明所依赖的全局交错合同。
• 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 对读：把 \(N\) 机、\(b/c\) 数组与整数 \(k\) 留在那一页；本页是两人、三枚变量的后至短注。
• 与 并发 对读：总览里的锁与死锁是教学装置；本页问的是两进程互斥是否必须复杂。
• 与 艾兹格·迪科斯彻 对读：人物页上的信号量、THE 与「goto 有害」都不是本页这两页纸；德克尔前驱写在 EWD 123，不是写在本注正文里。
• 与 顺序一致性 对读：先写后读的礼貌牌在弱模型上如何失去外观，是后文。
• 与 等待自由 对读：简单的阻塞互斥，并不能升格成停机也挡不住我的进展条件。
• 与 弗洛伊德 1967 对读：边上的归纳断言是另一种几何；本页选择了更短的操作论证，并把更重的断言证明留给 EWD 779。