形式陈述
固定异步共享内存模型:进程可能崩溃停止,正确进程持续取得步骤;实现可使用任意多个原子读写寄存器和某种线性一致的对象类型公理库并发对象Concurrent object可被多个线程并发调用并以顺序规格解释操作效果的共享对象。 。 的共识数 定义为:能够用这些对象为 个进程wait-free公理库Wait-free 进展Wait-free progress · Wait-freedom · 无等待进展每个正确参与者的每次操作都在有限个自身步骤内完成的个体级非阻塞保证。 地解决共识公理库分布式共识Distributed consensus · Consensus problem多个进程在可能故障和通信延迟下对一个值达成一致的任务。的最大 ;若对每个有限 都可解决,则记 。
这里分类的是对象类型及其完整顺序规格,不是某一个容量有限、随后耗尽的实例。算法可以创建任意多个 实例,原子寄存器始终作为辅助;进程必须在有限个自身步骤内决定,即使其他进程在任意时刻停止。若把 wait-free 换成 lock-free、允许阻塞锁,或改变操作返回值,得到的就不再是同一层级。
Herlihy 层级的经典分类包括:原子读写寄存器的共识数为 ;test-and-set、swap 与 fetch-and-add 的共识数为 ;标准比较并交换(CAS)公理库比较并交换Compare-and-swap · CAS原子地比较内存值并在相等时写入新值、同时返回比较结果的读改写原语。的共识数为 。数值不是“指令强度分数”,而是一个可实现性边界:共识数至少为 的类型可在至多 进程系统中,经由 wait-free 通用构造实现任意具有顺序规格且每次顺序操作都可在有限步骤内计算的对象;对于满足 的进程数 ,不存在只用 与寄存器为这 个进程 wait-free 实现 的方法,否则组合该实现与 的共识算法便会用 解出超过其共识数的共识,产生矛盾。
通用构造的核心是把并发操作转化为一串待决定的状态机步骤。各进程提出下一项操作,利用第 个共识对象唯一决定序列位置 的内容,再按共同前缀计算返回值;帮助机制公理库并发算法中的帮助机制Helping mechanism · Helping in concurrent algorithms · 并发帮助机制通过公开操作描述或可复用结果,使其他进程能够推进一个调用并为其完成提供证据的并发构造方法。使其他进程能够接手已经公布的调用,轮转优先规则再排除某个请求被永久跳过。具体构造还需处理操作描述、响应匹配与空间回收,但定理表达的是对象类型在给定进程数下的普适表达力。
直觉
共识要求多个进程从不同提议中不可撤销地选出同一个值,因此能测量原语“打破对称”的能力。普通读写让每个进程留下信息,却没有一个原子时刻能让竞争者共同认定谁先;CAS 则把“若仍无人决定,就由我写入”压成一次不可分割的条件更新,首个成功者自然成为共同选择。
层级的价值在于把无数实现问题缩成一次比较。若目标类型能解决三进程共识,而手头原语最多只能解决两进程共识,就无需继续寻找 wait-free 实现;不可能性已经来自组合论证。这个结论并不禁止锁实现或较弱进展实现,只精确排除指定模型中的 wait-free 路线。
例子与边界
用 CAS 为任意有限数量进程解决一次共识:共享原子槽 decision 初值为 ,其中 是提议值域之外保留的空标记;进程 执行 CAS(decision, ⊥, v_i),随后读取并决定槽中的值。只有一个 CAS 能把 替换为提议值,故所有进程读到同一决定;决定值确由某进程提出;每个进程只做常数次原子步骤,其他进程崩溃也不妨碍完成。在标准无限次可用、线性一致 CAS 语义下,这一构造对任意有限 成立。
固定二进程模型与价态
下面完整证明读写寄存器的二进程下界。[1, §3.1] 进程 是确定性的,输入各为一个bit,只能用任意多个多读多写原子寄存器通信。寄存器的初始内容固定且与输入无关;每个进程最初只知道自己的输入、身份和算法常量。一次步骤是读一个寄存器、普通写一个寄存器或本地状态转移。普通写不返回旧值;若返回旧值,它已经是swap,不在本证明的原语集合内。
本地步骤包括决定事件。等待也必须表示为可继续取步的本地动作,不能把阻塞后无动作当作完成。我们采用的wait-free条件包含:任意尚未决定的进程,从任意可达配置独自运行都能有限决定;在任意无限执行中,取得无穷多自身步骤的进程必已在有限前缀决定。无需假设两个进程都公平地继续运行。[1, §2.3]
配置公理库分布式配置Distributed configuration · Global configuration全部进程局部状态与通信介质状态组成的系统全局状态。 记录全部本地状态和共享寄存器;本地状态包括程序位置、读到的值和已经作出的决定。令
允许空延伸,因此已经作出的决定也算在内。wait-free保证 非空;若已有决定 ,一致性迫使它等于 。单价指 或 ,双价指 。若 表示执行有限步骤串 后的配置,则
所以单价只能保持,不能翻转。记 表示共享内存与进程 的本地状态相同;另一个进程的状态可以不同。确定性给出不可区分性引理:让 分别从 独自运行,它每次读到相同值,作相同写入,因而在相同步数决定相同值。这可对自身步骤直接归纳,不要求 。
从输入链找到初始双价
设 是输入为 的初始配置。有效性使 为0-单价, 为1-单价。考察
若三个配置全单价,就有相邻两个价态不同。第一对仅 的输入不同,第二对仅 的输入不同。让发生改变的进程永远不动,另一个独自运行;它在两次执行中的共享内存与本地状态相同,wait-free又要求它有限决定,故决定相同,与两边价态不同矛盾。因此至少一个初始配置双价。这一步使用私有输入与输入无关的初始共享内存,不能预先把全部输入写进公共状态。
为什么一定有临界配置
从初始双价配置出发,假如每个可达双价配置至少有一个立即后继仍双价,就始终选择这样的下一步,得到一条无限双价执行。只有两个进程,至少一个取得无穷多步;双价意味着始终没有人决定,违反wait-free。
所以存在可达双价配置 ,其中两个进程各自下一步 都进入单价。所有导致决定的延伸都必须先走其中一步,故
两边不能是同一个单值集合。交换 名称后,可设 属于 、 属于 ,并且 为0-单价、 为1-单价。因此 仍0-单价, 仍1-单价。以下穷尽两步可能的读写类型,证明这样的 不存在。
情形一:步骤可交换
若某一步纯本地,或两步访问不同寄存器,或两步都读同一个寄存器,两种次序产生完全相同的配置:
原因是两步的读返回值、写入内容及两个本地后继都相同。一个配置却被要求同时0-单价和1-单价,矛盾。本地决定也在此情形:若执行它已造成两个不同决定,则更直接违反一致性。
情形二:同一个寄存器,一读一写
设 是 读 , 是 普通写 。比较的不是两种执行次序,而是
的读没有改变共享内存, 在两条路径中做的是同一次写,写后自己的状态和全部共享内容相同。让 从1-单价的 独自运行,它必决定1;从0-单价的 也会作同一决定,矛盾。若 已决定,所需独自延伸就是空串。
对称地,若 为 写、 为 读,则 。让 从 独自决定0,就会从1-单价的 也决定0,同样矛盾。
情形三:同一个寄存器,两次普通写
设 把 写为 , 把它写为 。在 中第二次写覆盖了第一次;与直接执行 相比, 的写没有读取或返回被覆盖的旧值,故
这里不能写成 : 的程序位置已不同。只需 无法区分,就能复用上面的独自运行矛盾。即使 ,同样成立。
三类情形已穷尽所有原子步骤,反设协议不存在。一个进程直接决定自己的输入即可解共识,所以读写寄存器的共识数恰为1。增加寄存器数量、容量或本地计算不会破坏上述论证;增加一次能读取旧值的原子更新则会改变关键情形。
返回值和进展条件改变了什么
有限位宽、可能回绕的机器 CAS 是否保持抽象类型的全部能力,要看对象规格与可用内存模型。硬件吞吐、缓存争用和 ABA 风险影响实现性能与安全证明,却不改变理想原子 CAS 类型的经典共识数;若接口改成可能伪失败、只比较受限状态或允许非线性行为,就必须重新分类。
推论与应用
共识层级解释了读改写原语公理库读改写原语Read-modify-write operation · RMW将读取旧状态、依据旧状态决定更新及返回结果合为一个原子状态转移的同步原语;其内存序和进度保证需另行规定。之间并非只有性能差异。它为无锁数据结构给出选择下界,也说明为什么从弱原语实现强对象时,算法常不得不降低进展保证、限制参与者数量或引入更强硬件操作。
分类结论不能反向代替具体算法证明。一个原语共识数足够高,只表示存在通用 wait-free 构造;实际队列或栈仍需证明线性一致性、步骤界和内存回收。相反,某对象无法用低层原语 wait-free 实现,也不排除使用互斥锁公理库互斥锁Mutex · Mutex lock · 互斥量以获取、释放与所有权封装临界区互斥的同步对象。、随机化或特定调度假设得到可用实现。
上述证明和FLP公理库FLP 不可能性定理FLP impossibility · Fischer–Lynch–Paterson theorem完全异步系统中即使只允许一个进程崩溃,也不存在保证所有可容许执行终止的确定性共识协议。都用双价与不可区分性,但模型不同:这里是共享原子寄存器与个体wait-free,FLP处理可靠消息传递与公平无限执行。前者不是把后者换几个名词所得的直接推论。[1, §3.7] 随机共识公理库随机共识与概率一终止Randomized consensus · Ben-Or randomized consensus · 随机化共识固定不看随机位的异步调度器,完整证明两阶段随机二值共识的安全性、概率一终止和几何轮数尾界。再把终止改为对规定调度器以概率1成立,同时保留逐执行的安全性;它也不反驳此处的确定性下界。
参考资料
[1] Maurice Herlihy, “Wait-Free Synchronization”, ACM TOPLAS 13(1), 1991, pp.124–149,DOI 10.1145/114005.102808:§2.3的wait-free定义、§3.1 Theorem2的寄存器下界、§3.7的消息/共享内存模型区别。本页逐项展开初始输入链、临界配置存在性与所有读写配对。
[2] Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012,Ch. 5。
[3] Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004,共享内存可解性相关章节。