Herlihy–Wing 1990:线性化怎样把并发对象收成合法的顺序历史
Linearizability: A Correctness Condition for Concurrent Objects
1990 年 7 月,莫里斯·赫利希(Maurice P. Herlihy)与珍妮特·温(Jeannette M. Wing)在 ACM Transactions on Programming Languages and Systems 第 12 卷第 3 期发表《Linearizability: A Correctness Condition for Concurrent Objects》,页码 463 至 492。DOI 为 10.1145/78969.78972。对象是一份已发表的正确性条件:并发对象上的每一次操作,都应当看起来在调用与返回之间的某个时刻原子地生效;把这些生效点排成一条顺序历史,这条历史必须属于该对象的合法顺序规格,并且尊重实时先后——若操作 \(A\) 的返回事件发生在操作 \(B\) 的调用事件之前,线性化里 \(A\) 必须排在 \(B\) 前面。重叠被允许,虚构的是那一个瞬间;规格被给定,检验的是并发历史能否被收成规格里的成员。
它不是 分布式共识算法。状态机复制把客户端命令排成一条日志,再让各副本按同一顺序执行;那是在使用一份顺序规格,本页写的是规格应当满足的条件本身。它也不是 etcd:ReadIndex 与租约读是把「读也要像线性化」安装到 Raft 集群上的工程装置,本页不写心跳、租约时长、磁盘顺序。它更不是 ZooKeeper 那篇协调内核:ZooKeeper 把允许客户端同时挂起多个未完成请求的变体称作 A-linearizability,并声称满足它的系统也满足赫利希与温原来的线性化;那是后来的方言,不是 1990 年的定义。数据库事务 的可串行化谈的是多语句事务的交错,内存一致性模型 谈的是硬件与编译器对地址的可见顺序。两页都不是并发对象的这份条件。本页不是无锁算法手册,不是等待自由的菜谱,也不是 CAP 概览,更不是 Gray 1978 两阶段提交。等待自由的共识数分层见 Herlihy 1991。
破除误解:原子不是互斥,实时先后也不是可串行化
第一层误解把线性化听成「操作不准重叠」或「必须加锁」。论文允许调用区间在墙上时钟上相交。两个进程可以同时把请求送进同一个队列,调用尚未返回,另一个调用已经发出。线性化并不禁止这种相交,它要求的是:存在一种讲法,使得每一次操作都在自己的调用与返回之间的某一点上,像顺序规格里的一次原子步骤那样生效。那一点叫做线性化点。它是存在量词下的虚构瞬间,不必是源码里标出的某一行,更不必是互斥锁的临界区入口。锁是实现原子性的一种手段,线性化是观察者应当承认的效果。把条件读成「请用锁」,等于把规格收成配方,而本页拒绝配方。
第二层误解把线性化与莱斯利·兰波特 1979 年的顺序一致性当成同一个词。顺序一致性要求:全体操作看起来排成某一全局序列,且该序列尊重每个进程自己的程序序。它不要求尊重跨进程的实时先后。进程 \(P\) 的写已经返回,进程 \(Q\) 随后才发出读,顺序一致性仍然可以把这次读排到那次写前面——两边没有程序序把它们焊死。线性化多要的正是这一句:不相交的实时区间不得在顺序历史里颠倒。后果立刻可见。顺序一致性不是局部性质:每个对象各自顺序一致,组合成的系统仍可能不是。线性化是局部的:一个由若干对象组成的系统可线性化,当且仅当每个对象上的投影历史可线性化。组合性是这篇论文真正卖出的几何,不是「更强一致性」这句广告。把两者混称「强一致」,类型就错了。硬件上的顺序一致性合同见内存一致性模型那一页;本页的对象是程序员面对的并发数据类型,不是缓存行。
第三层误解把线性化收进数据库的可串行化。可串行化问的是:若干事务各自包含多步读写,交错执行的结果是否等同于这些事务按某一次序逐个跑完。事务是多操作的单元,对象操作是单次调用。克里斯托斯·帕帕季米特里欧 1979 年把可串行化写成并发数据库更新的正确性条件,讨论的是事务之间的冲突图与等价串行序;赫利希与温讨论的是单个并发对象的调用—返回历史。严格可串行化要求串行序还尊重事务的实时先后,它是线性化在「把一次事务看成一个粗粒度操作」时的近亲,仍然不是同一对象:粒度、组合方式、失败与中止的词汇都不一样。快照隔离可以挡住脏读,却放行写偏斜;那是隔离级别的故事,见数据库事务那一页。本页不把隔离级别表抄过来顶替定义。
第四层误解把这份条件收成等待自由或无锁算法的说明书。1991 年赫利希另写《Wait-free Synchronization》,对象是进展:一个慢的或停机的进程,不得永久挡住别人完成自己的操作,并由此排出共识数。1990 年这篇证明的是安全性一侧的可观察合同。论文里的「非阻塞」有精确而更窄的含义:作为正确性条件,线性化从不强迫一个尚未完成的调用去等待另一个尚未完成的调用先结束——若顺序规格在每个状态下都定义了该操作,总可以为这个挂起的调用补一个合法返回,使历史仍然可线性化。那是规格的完备性,不是 CAS 循环怎么写、退避怎么设。把非阻塞读成无锁菜谱,会把 1990 年的条件误认成 1991 年的进展层次,两篇论文的分工被抹掉。
历史与局部性:线性化点、顺序规格,以及组合为什么成立
装置从历史开始。一次执行被写成事件序列:某进程对某对象发出带参数的调用,稍后匹配一次带结果的返回。匹配按进程与对象对齐。顺序历史里,除了可能悬在末尾的那一次调用,每个调用都立刻跟着自己的返回,操作互不重叠。每个对象带着一份顺序规格:一组前缀封闭的合法顺序历史,队列、寄存器、集合各自不同。消息传递上把寄存器规格装出来的装置见 ABD 1995。并发历史要成为可线性化的,必须能被补全——给部分挂起的调用补上返回,丢弃其余尚未完成的调用——使得补全后的完整历史等价于规格里的某条顺序历史 \(S\),并且实时偏序嵌入 \(S\) 的先后。等价保留每个进程自己看见的事件序列。线性化点不是仪器读数,而是这条存在性陈述的简称:在调用与返回之间,可以指定一个生效瞬间,全体瞬间排成的序恰好是 \(S\)。
实时偏序只谈不相交。若 \(A\) 的返回事件在历史里出现于 \(B\) 的调用事件之前,则 \(A\) 在实时上先于 \(B\)。相交的操作在偏序里不可比,线性化可以按规格需要任选先后,只要结果仍合法。寄存器的旧读因此被钉死:写已经返回之后才发出的读,不得读到写之前的值,因为实时已经把写放在读前面,规格又禁止读到过期。队列同样:先完成的入队必须在顺序规格里排在后开始的出队能看见的位置上。允许相交,是为了并发;钉住不相交,是为了不让「已经结束」被后来者假装没发生。把线性化点画成日志里的墙钟时间戳,会把存在量化成一次测量;论文要的是相容性,不是授时。
挂起的调用如何补全,决定了「正在发生」的操作能否进入顺序历史。进程发出入队、尚未返回时,观察者有两种合法选择:补一个成功返回,让这次入队出现在线性化里;或者丢弃这次调用,当它从未生效。两种选择都必须保住已经完成的操作的实时先后,以及规格的合法性。作为条件的非阻塞在这里起作用:一次尚未返回的入队,不得强迫另一次已经返回的出队去等待它。若出队已经返回了空,那次尚未完成的入队就不能被补到这次出队之前,否则规格会出现「空出队发生在先入队之前」;它只能被丢弃,或排到这次出队之后。补全不是任意改写历史,而是在区间端点约束下选出一个仍合法的瞬间。
局部性把对象从系统里拆出来。系统历史在对象 \(x\) 上的投影,只保留涉及 \(x\) 的事件。定理说:整体可线性化,当且仅当每个对象的投影可线性化。证明的方向并不对称。若整体已经可线性化,投影继承那条顺序历史,显然各自合法。反过来才是几何:每个对象各自选出一条尊重自身实时偏序的合法顺序历史,再把这些顺序在全局事件上拼合。因为不同对象的事件除了经由进程程序序间接相遇外并不共享状态,拼合不会发明新的对象内部矛盾;实时偏序本来就已经按对象分开。于是模块化成立。你可以单独证明队列可线性化、寄存器可线性化,再把它们放进同一个进程,不必重新对整个堆做一次全局排序论证。顺序一致性做不到这一句:它的全局序必须同时满足所有进程的程序序,投影会丢掉那些跨对象的约束,局部成立推不出整体成立。这篇论文把组合性写成定理,而不是写成软件工程口号。
它证明了什么,也就划出了它没有证明什么。它证明:并发对象的正确性可以写成对历史的存在性条件;该条件尊重实时先后、服从给定的顺序规格,并且对对象分解是局部的;作为条件,它不强迫挂起的调用互相等待。它没有证明任意对象都存在等待自由实现——那是次年共识数的工作,本页不写层次表。它没有给出线性化点应当插在比较并交换的哪一次重试上,没有比较哪一种无锁队列更快,也没有把副本如何对日志达成一致写成协议。状态机复制可以实现线性化的共享对象,实现所用的共识算法是另一页的对象。它没有给芯片写内存模型,没有把缓存一致性协议收进并发对象,也没有讨论分区时该牺牲哪一侧——CAP 不是本页的定理。顺序规格被当作给定:队列是什么,由规格说了算;论文检验的是并发观察能否被收进规格,并不发明业务语义。ZooKeeper 后来把多挂起请求的方言标成 A-linearizability,etcd 后来用 ReadIndex 去逼近线性化读,两者都引用这份条件,都不代替这份条件。把引用误认成本页变厚,会把规格写成集群操作单。
跨域连接
- 时间哲学:线性化点不是墙上时钟的一格,而是给每个调用区间选出的代表元。实时先后接近 B 系列里的「先于」:返回已经发生,调用尚未发出,两者不相交。相交的操作没有客观的先后,线性化允许在规格许可的范围内指定一个。奥古斯丁说「现在」没有厚度;线性化点同样没有必须可观察的厚度,它只保证存在一种不违反区间端点的讲法。把「最终生效」听成「再等一会儿就能看见那一毫秒」,会把存在量词还原成超时,条件塌回工程里的等待。本页的时间是历史上事件的排列,不是授时服务发出的时间戳。
- 认识论:外部观察者只看见调用与返回,看不见生效瞬间。线性化不是关于「我已经看见原子步骤」的报告,而是关于可能世界的存在断言:存在一条与全部观察相容、且属于规格的顺序历史。单个进程完成一次操作,并不因此拥有那条全局历史的知识。把「我的调用返回了」误认成「所有人都已经按这个顺序知道了这件事」,是把局部证据提升为公共知识。工程事故常发生在这一跃:本地成功被当成集群已经线性化的证明。规格要求的是存在性,不是每个参与者都持有同一份已核验的全序抄本。
- 同一性:并发对象与顺序对象在什么意义上是同一个东西?赫利希与温的答案不依赖共享同一段内存,而依赖外延:所有可观察的并发历史都能被收成那份顺序规格的成员。对象在并发下不断改换内部交错,却仍被认作「那个队列」,凭的是规格给出的同一标准,而不是某次运行的内部布局。这与持存问题结构相似:变化中的个体凭什么还是它。换一套内部表示、甚至换成一组副本,只要历史仍可线性化到同一规格,同一性在正确性条件的意义上保持。规格若改——队列变成「有时允许越过」——对象就不再是原来那个。
- 因果:实时先后不是休谟要你在台球桌上找出的那根「使之运动」的力,也不是兰波特消息里的 happens-before。你看见的是两次事件的不相交:一次返回结束了,另一次调用才开始。中间没有必须经验到的传递物。线性化要求把这种不相交提升为规格里的先后,使后来的操作不得假装先发生的事没有发生。消息因果可以比实时更弱,延迟让「先发送」不必「先到达」;硬件上的可见性又是另一套合同。休谟说你看不见必然连接;线性化也承认你看不见生效点,只要求存在一种不拆开已结束区间的叙述。把实时先后读成物理因果,会把墙上时钟误当成规格的发动机。
- 知识:单价配置是系统已经把答案写成公共事实的状态。线性化并不直接生产这种公共事实:它只约束「若把观察收成顺序历史,历史必须合法」。学习者可以完成一次读并返回一个值,却仍不知道别人的未完成写将插在哪一个线性化点上——只要那些写的区间仍与这次读相交。相交意味着知识尚未闭合;不相交才把先后钉死。把尚未闭合的交错当成已经共享的全序,会把安全性失败误诊成「慢」,也会把活性上的等待误诊成分叉。分叉是两条合法顺序历史无法再被同一规格收容;等待只是相交尚未结束。本页的条件管的是前一种错误不得发生,不管时钟把相交拉得多长。
参考文献
- 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, "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. —— 顺序一致性,用以标明本页多要的是实时先后与局部性。
- Christos H. Papadimitriou, "The Serializability of Concurrent Database Updates", Journal of the ACM 26(4), 1979, pp. 631–653. DOI: 10.1145/322154.322158. —— 可串行化,用以对照事务交错与单对象操作不是同一条件。
- Maurice Herlihy, "Wait-free Synchronization", ACM Transactions on Programming Languages and Systems 13(1), 1991, pp. 124–149. DOI: 10.1145/114005.102808. —— 次年进展条件与共识数,用以标明本页停在安全性一侧。
- Bowen Alpern & Fred B. Schneider, "Defining Liveness", Information Processing Letters 21(4), 1985, pp. 181–185. DOI: 10.1016/0020-0190(85)90056-0. —— 安全与活性的极限闭包口径,线性化作为安全性质的背景。