Dijkstra 1965：互斥怎样在没有仲裁者的共享变量上写成可推理的问题
Solution of a Problem in Concurrent Programming Control
1965 年 9 月，艾兹格·威贝·迪科斯彻（Edsger W. Dijkstra）在 Communications of the ACM 第 8 卷第 9 期发表《Solution of a Problem in Concurrent Programming Control》，整整一页，页码 569。DOI 为 10.1145/365559.365617。作者单位印作荷兰埃因霍温理工大学（Technological University, Eindhoven）。对象是一份已发表的问题—解—证明：\(N\) 台计算机共用一块存储器，每台跑一段可看成循环的程序，循环里有一截临界区；只用共享的整型与布尔变量，在没有中央仲裁者的前提下，保证任意时刻至多一台处于临界区。读写一个字被规定为不可分割；多台同时碰同一单元时，这些往来会一个接一个发生，次序未知。论文自述该问题至少自 1962 年起未决，连是否可解都不清楚。封面把文章分成三截：问题、解、证明。
它不是 并发 总览。那一页讲线程、锁与信号量；本页停在这一页纸上的 \(N\) 机互斥合同。它不是 艾兹格·迪科斯彻 的人物页，不是 1968 年「goto 有害」，不是 THE 操作系统，不是信号量，也不是银行家算法。它更不是 兰波特 1974 年的面包店算法。后来把两进程写成两面旗加一个 \(TURN\) 的短注，见 Peterson 1981。它不是 线性化，不是 等待自由，不是 事务内存，不是线程库或锁省略，也不是布置或绕过互斥的操作单。两进程上的正确前驱，迪科斯彻后来点名为荷兰数学家 T. J. 德克尔（Th. J. Dekker）；本页 CACM 正文并不写出这个名字，它把人数从 2 推到 \(N\)。
破除误解：互斥不是锁指令，活性也不是每人轮到
第一层误解把 1965 年听成「请调用互斥锁」或听成芯片上的测试并设置。论文允许的往来只有把一个字写入公共存储，或非破坏地读出一个字。if b[k] then k := i 在文中是复合句，不是一条原子的读改写。你先看见一个布尔，再决定是否改写那个整数；中间别人可以插进来。困难正在这里：每台计算机一次只能发出一条单向消息。把本页收成测试并设置的使用说明，等于把问题里禁止的原语提前发下来。信号量是后文的抽象；本页还没有那一层，它问的是共享变量本身够不够把互斥写成可检查的推理。
第二层误解把德克尔的两进程解与本页收成同一张配方，或反过来以为 1965 年凭空发明了互斥。迪科斯彻在稍后的技术报告《协作的顺序进程》（EWD 123，1968 年收入 Genuys 主编的 Programming Languages）里写明：许多人试过，一批解被证明是错的，有人开始怀疑根本不可解；第一个正确的两进程解应归功于德克尔。德克尔把「安全闸门」与一个只在两人谁也不立即成功时才出面打破平局的整数 turn 混在一起。本页的对象是把同一类约束推到 \(N\) 台：对称、不靠相对速度、临界区外停机不得卡住别人、不允许把「您先请」拖到永远。把两人解直接复制 \(N\) 份，并不自动满足这些句子。点名德克尔是为了标明前驱，不是把 1965 年这一页读成德克尔论文的转载。
第三层误解把条件 (d) 听成「每一个想进的人终将进入」，或听成后来的等待自由。论文要排除的是：给一批已经靠近入口的计算机安排有限速度，使「谁先进入」被推迟到永恒；「您先请—您先请」即使少见，也不算合格。这是关于集体的进展：临界区空着、又有人在入口打转时，不能全体永远进不去。它不担保某一个编号不会被别人无限次超过。唐纳德·克努斯 1966 年在同一本期刊写了半页评论，构造了一种调度：一台计算机可以一直想进，却看着别人反复完成临界区。互斥作为安全性可以仍成立；饿死作为个体活性则失败。把 (d) 读成公平，会把一页里实际写下的量词撑大。等待自由还要更强：别人停机也不得挡住我。互斥按定义违反它。本页安装的正是「必须有人先出来」的装置。
第四层误解把标题听成生产环境的同步手册，或听成已经给出现代内存模型下的可移植写法。论文假定公共存储上对同一单元的读写会排成某种未知次序，证明则用「先写下自己的 \(c\)，再看别人的 \(c\)」这种全局讲法。顺序一致性 要到 1979 年才被写成多处理器合同；弱模型上同一套布尔可以同时看见对方的旧值，朴素的「先写后读」互斥会一起进入临界区。本页不把屏障、锁前缀或缓存协议写进 1965 年。它也不把 弗洛伊德 1967 的边上断言当成自己的证明几何：迪科斯彻用的是关于谁在打转、\(k\) 何时停止改写的操作论证，结尾甚至写「作者相信这就完成了证明」。把这一页听成可上线的临界区模板，或听成已经机器检查过的验证条件，类型都错了。概念证据到此为止，不是配方。
1965 年的装置：公共字、四条禁令，以及一页里的论证
问题从 \(N\) 台计算机说起。每台从事一个可看成循环的过程；每个循环里出现所谓临界区。要编程使得任意时刻这 \(N\) 个过程里只有一个处于临界区。通信手段只有公共存储：写入一个字、非破坏地读出一个字，都不可分割；多台同时碰同一单元时，往来依次发生，次序事先不知道。作者请读者在这里停住自己试一试：否则很难体会「一次只能请求一条单向消息」有多绕，也很难明白这个问题远非平凡。
解必须满足四条。(a) 在 \(N\) 台之间对称，因此不许引入静态优先级。(b) 不得对相对速度作任何假定，甚至不得假定速度在时间上恒定。(c) 任一计算机在临界区外相当远处停住，不得造成他人被堵住的可能。(d) 若不止一台即将进入临界区，则不可能为它们设计出这样的有限速度，使「谁先进入」被拖到永恒。换一种说法：仍可能「您先请—您先请」的构造，哪怕这种堵塞不常见，也不算有效解。对称排除了「一号永远优先」这种仲裁者的简化版。速度独立排除了靠延时碰运气。(c) 排除了简单轮转：若下一棒的人在剩余段里停死，别人会跟着死。(d) 排除了礼貌活锁。四条合在一起，才逼出后来被叫做「只用原子寄存器做互斥」的那一类对象。
公共存储由布尔数组 \(b,c[1:N]\) 和一个整数 \(k\) 组成。\(k\) 落在 1 到 \(N\) 之间。\(b[i]\) 与 \(c[i]\) 只由第 \(i\) 台计算机赋值，供别人检查。假定所有计算机都在临界区外相当远处启动，上述布尔数组全为真；\(k\) 的初值无关紧要。第 \(i\) 台的程序被标成若干语句标号。它先把 \(b[i]\) 写成假，表示自己已离开可停机的剩余段、开始一次进入尝试。若当前的 \(k\) 不是 \(i\)，它把 \(c[i]\) 写成真——撤回自己在第二道门上的声称——并在看见 \(b[k]\) 为真时把 \(k\) 改成 \(i\)，然后回到对 \(k\) 的判断。若当前的 \(k\) 已经是 \(i\)，它把 \(c[i]\) 写成假，再扫描其余每一台的 \(c\)；只要发现某一台的 \(c\) 为假，就跳回对 \(k\) 的判断。只有这次扫描走完、没有跳回，它才进入临界区。离开临界区时先把 \(c[i]\) 写成真，再把 \(b[i]\) 写成真，然后进入「允许停机」的剩余循环，之后再开始下一轮尝试。
\(b[i]\) 为真表示第 \(i\) 台目前不在进入尝试里；\(c[i]\) 为假表示它自以为已被提名、正在第二道门上检查别人。\(k\) 是动态提名，不是静态优先级。本页复述这些职务，是为了让一页里的证明能被跟上，不是一份把赋值抄进线程库的清单。
证明先主张安全性：不会有两台同时处于临界区。理由是，进入临界区的唯一途径，是在把自己的 \(c\) 写成假之后，发现所有其他的 \(c\) 都为真。若两台都完成了这件事，则各自的 \(c\) 都为假，后检查的那一台应当看见先写下假值的那一台。论文把这句话写得很短，没有按交错逐条展开。它依赖的是：对同一单元的读写排成一条未知次序，并且「先写自己的 \(c\)、再读别人的 \(c\)」在证明的讲述里被当成一种可比较的先后。这种讲述要到 顺序一致性 才有名字。1965 年把它当作公共存储的直观。
证明的第二截针对 (d)：当没有计算机处于临界区时，在入口打转（跳回判断 \(k\) 的那一处）的计算机里，至少一台——因而恰好一台——将及时被允许进入。若当前的第 \(k\) 台不在打转者之列，则 \(b[k]\) 为真，打转者都会看见 \(k \neq i\)。于是其中一台或多台会在检查 \(b[k]\) 时决定执行 \(k := i\)。第一次这样的赋值之后，新的 \(b[k]\) 变成假，不会再有计算机重新决定去改 \(k\)。等所有已经决定的赋值都做完，\(k\) 会指向打转者中的某一个，并且暂时不再改变——直到这台完成临界区、把 \(b[k]\) 写回真。一旦 \(k\) 不再改变，被指向的那一台就在第二道门上等待所有其他 \(c\) 变为真；若这种情况尚未出现，也一定会出现，因为其余打转者发现 \(k \neq i\)，被强迫把自己的 \(c\) 写成真。论证到此，作者相信证明完成。它解释了为什么不会全体永远互相谦让，没有解释某一个固定编号为何不会永远当那个「别人」。把两截证明读成公平，会把一页纸没有写下的全称量词塞进去。
它证明了什么，没有覆盖什么
它证明了：在「字的读写不可分割、同单元同时往来排成未知次序」这一装置上，\(N\) 台循环程序的临界区互斥不是不可做的开放问题；存在一种只用布尔数组与一个整数、不设静态仲裁者的构造；该构造按作者的论证满足对称、不靠速度、临界区外停机不堵塞，并且排除「您先请」式的无限推迟。意义首先是存在性：计算机耦合里那些看起来学院派的逻辑问题，有一份可以写在一页上的解。作者自己也把「这个问题确实可解」当成应被重视的事实。
它没有证明个体不会饿死。克努斯 1966 年的评论给出调度，使一台计算机的进入被无限推迟，同时别人反复进入。后来的面包店算法用号码追求一种更强的先来先服务；那是 1974 年的另一份对象，见 Lamport 1974，假设更弱，合同更强，不是本页的补丁。它没有给出测试并设置、比较并交换，也没有把互斥收成操作系统里的一种系统调用。信号量、哲学家进餐与银行家算法属于 迪科斯彻 随后几年的另一条工作，封面不同。
它没有覆盖 线性化：临界区是一段程序文本，不是对象上带调用—返回区间的生效点。它没有覆盖 等待自由：持有临界区或停在入口协议里的进程，按设计可以挡住别人；等待自由拒绝这种挡住。它没有覆盖 内存一致性模型 在弱序下哪些布尔互斥会失效。它没有把 归纳断言 写到这些标号的边上，也没有给出模型检验脚本。本页不提供如何把上述赋值抄进 pthreads、如何布置锁省略、如何让互斥失效或绕过临界区的步骤。一页回答的是「没有仲裁者时互斥能否被推理」；克努斯回答的是「集体进展不等于个体公平」。两句都不是操作单。
跨域连接
- 证明：迪科斯彻把全文收成问题、解、证明三截，等于承认：一段并发控制若不能被论证，就不算解。可是这份证明是操作叙事，不是从公理到定理的形式推演。安全性靠「进入当且仅当自己的 \(c\) 为假且看见其余为真」一句话；活性靠 \(k\) 在有限次赋值后冻结。结尾的「作者相信」标明证书尚未闭合。克努斯并没有推翻互斥那一句，他造了一个调度，使另一句未被写出的全称命题失败。数学里的证明要求量词写全；并发里最常见的事故，正是把「不会全体卡住」听成「每一个人都轮得到」。
- 认识论：条件 (b) 拒绝一种求知程序——先测出别人有多快，再决定自己是否进入。完全不知道相对速度时，沉默既可被当成「他已在临界区外停机」，也可被当成「他只是慢」。条件 (c) 进一步禁止把「我看见他很久没写」当成「我可以假定他永远不会再要进入」的证据：停在剩余段的人不得成为堵住别人的理由。你能够合法使用的，只有公共存储里已经写下的字。把尚未观察的速度提升为关于他人意图的知识，正是这篇要排除的那类解。互斥在这里首先是一份关于许可何种证据的合同，其次才是一组布尔。
- 等待自由：1991 年的尺从反面量这篇。等待自由要求我完成自己的操作只靠自己的有限步，哪怕别人已经停机。临界区按定义把别人的进入交给我何时离开；若我停在里面，等待者永远进不去。本页的 (c) 只保护停在临界区外的人，并不保护停在临界区里的人，更不保护停在第二道门半道上、已经把 \(c\) 写成假的人。赫利希后来证明：只用寄存器，两个进程甚至无法等待自由地达成共识。1965 年能做成的，恰好是一种必须阻塞的协调。把「迪科斯彻已经解决了并发控制」听成「共享变量上一切进展条件都已解决」，会把互斥的存在性证明误认成共识数表的底端。寄存器够写互斥，不够写两人的等待自由共识——两句话可以同时真。
- 自由：对称性禁止把某台计算机写成永久的立法者。没有静态优先级，意味着谁都不得预先占有「先进入」的权利；\(k\) 只是临时提名。可是互斥本身又是一种严格的消极自由：当我处于临界区，别人进入的自由被暂停。暂停有期限，前提是我终将离开。若把「不得被静态排到末位」与「不得在我想进时被无限超过」当成同一句自由，克努斯的调度就会被看成无关的边角。前者是这篇写下的对称；后者是这篇没有担保的公平。去掉仲裁者，并不自动得到每人轮到的权利。
- 顺序一致性：1965 年的公共存储合同只把「同一单元上的同时往来」收成未知次序。证明里用到的先后，却常常跨过两个单元：先写自己的 \(c\)，再读别人的 \(c\)。若机器允许这两步在另一台计算机看来颠倒，安全性那句短论证就不再能从装置里推出来。兰波特 1979 年把「看起来像某一条尊重程序序的交错」写成多处理器必须承认的外观，并证明单处理器各自顺序并不足够。本页的互斥是那篇短注里反例的亲戚：跨单元的先写后读，正是弱可见性最先咬住的模式。1965 年尚未把合同命名；1979 年命名的是让 1965 年那种讲述合法的条件，不是把这一页改写成芯片手册。
参考文献
- 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\) 计算机临界区互斥的问题、共享变量解与一页证明。
- E. W. Dijkstra, "Cooperating Sequential Processes", in F. Genuys (ed.), Programming Languages, Academic Press, 1968, pp. 43–112. —— 点名德克尔给出首个正确的两进程解，并把本页的 \(N\) 机问题放进更长的进程协作论述；手稿为 EWD 123。
- Donald E. Knuth, "Additional Comments on a Problem in Concurrent Programming Control", Communications of the ACM 9(5), 1966, p. 321. DOI: 10.1145/355592.365595. —— 指出个体可被无限超过，用以标明本页 (d) 不是饥饿自由。
- 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. —— 等待自由与共识数，用以标明互斥装置恰好落在该尺的反面。