Lamport 1979：顺序一致性怎样把多处理器程序收成某一条尊重程序序的交错

破除误解：顺序一致不是缓存连贯，也不是线性化，更不是 1978 年的先于关系#

第一层误解把顺序一致性听成缓存一致性。缓存一致性按单个地址说话：对同一单元的写应当排成一条，读应当看见这条线上最后一次写。顺序一致性按全体地址与全体处理器说话：还要尊重每个处理器自己的程序序，并把所有操作收进某一条全局交错。可以有连贯的缓存，却允许对两个地址的写在另一处理器上以相反顺序可见。论文的互斥例子恰恰跨过两个单元。把本页收成总线探听或目录协议的操作单，类型就错了。一致性协议是实现可见性的一种装置；本页问的是观察者应当承认的效果。单处理器流水线可以在内部打乱执行，只要对外仍像按程序序执行；把那一套内部重排直接接到共享存储上，并不自动得到顺序一致的多处理器。

第二层误解把顺序一致性与 线性化 当成同一个词。两者都要求「看起来像某一条顺序执行」，差别在约束。顺序一致性只钉住每个处理器内部的程序序，不要求尊重跨处理器的实时先后。一个处理器的写已经返回，另一个处理器随后才发出读，顺序一致性仍然可以把这次读排到那次写前面——两边没有程序序把它们焊死。线性化多要不相交的实时区间不得颠倒，并且证明该条件对对象分解是局部的。顺序一致性不是局部性质：每个对象各自顺序一致，组合成的系统仍可能不是。把两者混称「强一致」，会把 1979 年的多处理器合同收成 1990 年的对象规格。本页的对象是共享存储上的取数与存数，不是队列或集合的调用—返回历史。等待自由 谈的是进展，更不是本页的安全性条件。

第三层误解把 1979 年听成 Time, Clocks。年份只差一格，装置完全不同。1978 年的先于关系由进程内部次序与消息的发送—接收生成，用来给分布式事件编号。1979 年的偏序由「同一处理器按程序发出请求」与「同一存储模块上的先进先出队列」生成，用来证明取数看见的值能由某次顺序执行产生。没有消息，没有逻辑时钟，也没有把偏序延拓成全序去排队资源。把 happens-before 读进本页，会把共享存储误当成邮路。把本页读成授时或向量时钟，同样错了。论文甚至把专用通信寄存器也写成可以看作单独的存储模块：通信仍被收成对单元的访存，而不是收成 1978 年那种消息事件。

第四层误解把标题听成一份造芯片的配方，或听成「每个处理器自己顺序执行就够了」。论文开篇就拆开这两句。高速处理器可以按与程序不同的次序执行操作；只要结果与按程序序执行相同，该处理器仍被称为顺序的。由若干这样的顺序处理器去访问公共存储，并不保证整个多处理器顺序一致。证明多进程算法正确的惯用方法，预先假定了顺序一致性；若机器不提供它，那些方法不能被依赖。论文给出的 R1 与 R2 是充分条件，用来保证：若各处理器是顺序的，则整机顺序一致。它们不是必要且充分的现代内存模型公理，不是写缓冲与失效队列的产品页，也不是教人如何在弱模型上布置屏障的手册。本页拒绝把充分条件写成侵入步骤，也拒绝把互斥协议写成可上线的同步配方。

定义、互斥例子，以及两条充分条件#

顺序处理器的合同只有一句：一次执行的结果，与把操作按程序规定次序执行所产生的结果相同。多处理器的顺序一致性在此之上再要一句：还存在某种把全体处理器操作排在一起的序列，使得结果与按该序列执行相同，并且每个处理器的操作在该序列中仍按其程序次序出现。「某种」是存在量词。规格不指定哪一条交错被选中，只要求存在一条合法交错，能够解释这次执行看见的全部值。并发 允许各处理器同时发出请求；顺序一致性约束的是这些请求的可见效果，不是墙上时钟的同时性。交错是解释，不是测量到的唯一物理时间线。

论文用一个两进程互斥协议说明：单处理器顺序性不够。两个进程各有临界区，协议的目的是保证同一时刻只有一人进入。进程一先把单元 \(a\) 写成 1，再读取单元 \(b\)；若读到 0 则进入临界区。进程二对称：先把 \(b\) 写成 1，再读取 \(a\)。在顺序一致的机器上，这个协议的互斥可以按断言方法证明。论文把它留给读者，作为另一套证明练习的入口，具体技术指向兰波特 1977 年的断言证明与奥维基、格里斯 1976 年的公理方法。可是，若把进程一的程序单独拿出来看，「把 \(a\) 写成 1」与「读取 \(b\)」这两步对进程一自己的最终局部结果可以交换。先读取对方的单元再写自己的单元，两边都可能看见 0，两人同时进入临界区。于是得到第一条要求。这个例子是反例，用来标明合同缺了什么；它不是一份让互斥失效的操作单。

要求 R1：每个处理器按程序规定的次序发出存储请求。满足 R1 并不简单。存数只能在值被算出之后真正完成；处理器常常在还不知道前一次存数要写什么值时，就已经准备好发出下一次取数。为了少等，可以把存数请求先发到对应模块，值稍后补上。模块在收到值之前不得执行这次存数。发出请求与执行请求被分开，但发出次序仍须尊重程序序。这是论文写下的实现自由，不是把存储缓冲当成绕过程序序的许可。

R1 仍不够。论文设每个存储模块有若干端口，每端口服务一个处理器（或输入输出通道）。令 \(a\) 与 \(b\) 分住两个模块。可能发生如下交错。处理器一向模块一发出「\(a:=1\)」，该模块正忙于别人的操作。处理器一随即向模块二发出「取 \(b\)」，模块二空闲，取数开始执行。处理器二向模块二发出「\(b:=1\)」，排在刚才那次取数之后。处理器二再向模块一发出「取 \(a\)」，模块一仍忙。模块一现在有两笔等待。若它用轮转调度先服务处理器二的取数，则两人都可以进入临界区。出错的条件是：对同一模块的两笔请求，没有按它们到达的次序执行。于是得到第二条要求。

要求 R2：发往同一存储模块的全部请求，从单一的先进先出队列接受服务。发出一次请求，就是把该请求排进这支队列。R1 意味着：当前请求尚未入队之前，处理器不得再发下一个请求；队列满则必须等待。若两个处理器同时试图入队，谁先被服务无关紧要。论文加了一条注记：若一次取数所要的单元在队列里已有存数请求，取数不必再入队，可以直接返回队列中最后一次相应存数的值。这是把尚未执行的存数转发给后来的取数，不是绕过程序序，也不是一份投机执行清单。

R1 与 R2 合在一起，保证：若各处理器是顺序的，则整机顺序一致。证明先在存储请求上定义关系 \(A \to B\)：或者二者由同一处理器发出且 \(A\) 先发出；或者二者发往同一模块，且 \(A\) 先入队（因而先执行）。R1 与 R2 使 \(\to\) 成为偏序。再利用各处理器的顺序性，可证每一次取数与存数所看见或写下的值，都与按下述规则的某次顺序执行相同：凡 \(A \to B\)，则 \(A\) 排在 \(B\) 前面。这就是顺序一致性。关系是证明用的偏序，不是 1978 年那种由消息生成的潜在因果。

R2 还可以减弱。存储模块不必在队头那次存数尚未拿到值时整段空转；只需保证对同一存储单元的请求按队列次序服务。对不同单元的请求可以乱序。顺序一致性仍在，因为这种服务策略在逻辑上等价于把每个单元看成带自己队列的独立模块。若干单元共享硬件，只影响服务速率与队列容量，不影响顺序一致性这个逻辑性质。单元级的队列与模块级的队列，在规格里是同一句话的两种粒度。

它证明了什么，也就划出了它没有给出什么。它证明：多处理器正确执行多进程程序，不能从「每台处理器各自顺序」直接推出；需要一条关于全体操作的交错合同，以及一组足以推出该合同的互连条件。它没有给出缓存行、监听、目录或失效协议。它没有把后来的总存储序、弱序或语言内存模型写进 1979 年；那些总览见 内存一致性模型。它没有把 事务内存 的提交瞬间收进队列。论文自己写下代价：这些要求排除了一些用来加快单台顺序处理器的技术；对某些应用，为顺序一致性而拖慢处理器可能不值得。那时就必须意识到，设计多进程算法的惯用方法不能再被当成正确性担保。同步协议必须下到机器指令码的最底层去设计，验证正确性变成一项极其沉重的工作。那是警告，不是操作单。本页不提供如何布置屏障、如何改写临界区、如何用缓冲让互斥失效的步骤。定义回答的是「看起来像某一条尊重程序序的交错」；R1 与 R2 回答的是「一种足以推出该外观的互连」。两句都不是配方。

跨域连接#

• 时间哲学：顺序一致性里的那条全局序列不是墙上时钟的一格，而是规格里的代表元。程序序是每个处理器私有的先后；全局序列必须把这些私有先后嵌进去，却不必等于请求离开芯片的物理时刻。奥古斯丁说「现在」没有厚度；那条交错同样没有必须可观察的厚度，它只保证存在一种讲法，使已看见的值不与任何尊重程序序的顺序执行矛盾。把「最终可见」听成「再等一会儿就能读到那一周期」，会把存在量词还原成超时。本页的时间是历史上操作的排列，不是授时。
• 因果：取数返回一个值，看起来像被某次存数「撞」出来的。观察者实际看见的是程序发出的次序，以及同一模块队列上的入队次序。中间没有必须经验到的传递物。休谟说你看不见必然连接；轮转调度可以把先到达的请求放到后服务，使互斥协议在没有 FIFO 时失败。论文把「使之可见」收成入队关系，而不是收成总线上的撞击。实时上谁先把电信号送到端口，并不自动等于规格里谁先执行。把端口竞争读成台球，会把调度误当成物理力。本页的因果是证明里的偏序：能由程序序与 FIFO 生成，也就能解释取数看见的值。
• 认识论：每台处理器各自顺序，是关于局部执行的合格证据，却不是关于整机的知识。论文开篇的要点正是这一跃不成立：局部正确不能推出全局正确。要主张「这次多进程执行是正确的」，还需要关于全体操作如何交错的额外证成。R1 与 R2 是这种证成的一种充分条件，不是观察者已经持有的那条全局序列。单个处理器完成一次取数，并不因此看见那条交错。把「我按程序序发出了请求」提升为「整机已经顺序一致」，是把欠定证据做成知识。
• 知识：取数返回的值，还不是别人能够持有的公共事实。顺序一致性只说：存在某一条尊重程序序的顺序解释，与这次执行相容。没有人被要求持有那条序列的抄本。进程一读到 \(b=0\)，并不等于知道进程二尚未发出写，更不等于共同知道「临界区现在空着」。相交的请求使知识尚未闭合；FIFO 只约束同一模块上已经入队的先后。把局部返回误认成已经共享的全序，会把安全性失败误诊成「慢」。本页管的是可见历史能否被收成合法交错，不管谁觉得自己已经知道。
• 线性化：1990 年把并发对象的正确性写成调用与返回之间的生效点，并要求不相交的实时区间不得颠倒。1979 年没有调用区间，也没有对象上的投影定理。它的全局序列只嵌程序序，因此缺少线性化用来换取局部性的那一句实时约束。两个条件都拒绝把「看起来顺序」写成互斥锁配方，但卖出的几何不同：一个是共享存储上的多处理器合同，一个是可组合的对象规格。把本页读成线性化的简写，会把十年后的局部性定理提前塞进两页短注。

参考文献#

• 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. —— 本文对象：顺序处理器、顺序一致性定义，以及充分条件 R1、R2。
• E. W. Dijkstra, "Hierarchical Ordering of Sequential Processes", Acta Informatica 1, 1971, pp. 115–138. DOI: 10.1007/BF00289519. —— 论文引用的多进程算法设计出处之一。
• Leslie Lamport, "Proving the Correctness of Multiprocess Programs", IEEE Transactions on Software Engineering SE-3(2), 1977, pp. 125–143. DOI: 10.1109/TSE.1977.229904. —— 论文把互斥证明留给读者时指向的断言技术。
• Susan Owicki & David Gries, "Verifying Properties of Parallel Programs: An Axiomatic Approach", Communications of the ACM 19(5), 1976, pp. 279–285. DOI: 10.1145/360051.360224. —— 论文引用的并行程序公理方法。
• Maurice P. Herlihy & Jeannette M. Wing, "Linearizability: A Correctness Condition for Concurrent Objects", ACM Transactions on Programming Languages and Systems 12(3), 1990, pp. 463–492. DOI: 10.1145/78969.78972. —— 用以标明本页不要求实时先后，也没有对象上的局部性。
• Leslie Lamport, "Time, Clocks, and the Ordering of Events in a Distributed System", Communications of the ACM 21(7), 1978, pp. 558–565. DOI: 10.1145/359545.359563. —— 用以标明本页的偏序不是消息上的先于关系。

延伸阅读#

• 与 内存一致性模型 对读：那一页从本页的定义出发，再写芯片几乎从不提供裸的顺序一致性。本页不写总存储序与语言级合同。
• 与 线性化 对读：先看共享存储上的程序序合同，再看并发对象怎样多要实时先后与局部性。
• 与 1978 时钟 对读：消息偏序与存储队列偏序不要收成同一种「时间」。
• 与 计算机体系结构 对读：单处理器可以对外像顺序执行；接到共享存储之后仍缺本页这一句。
• 与 并发 对读：同时发出请求是事实；本页约束的是可见交错，不是锁的写法。
• 与 事务内存 对读：提交瞬间不是 FIFO 队列；仿真可以停在顺序一致，那是后文。
• 与 等待自由层级 对读：本页是安全性一侧的外观，不是进展与共识数。