线性一致性证明 | Codeboy's Blog

形式陈述

给定一个具体并发对象和原子顺序规格，先对观察到的有限历史 $H$ 处理未决调用：构造扩展 $H'$ ，保留所有已经返回的操作，并可在 $H$ 末尾为任意一部分 pending 调用追加匹配响应；其余 pending 调用从 $\operatorname{complete}(H')$ 中删去。要找到合法顺序历史 $S$ ，使

\operatorname{complete}(H')\equiv_{\mathrm{proc}}S, \qquad {<}_{H}\subseteq{<}_{S}.

第一式逐进程保留调用、参数、响应与结果，第二式保留 $H$ 已经确定的实时先后。已经完成的调用不能被 completion 删除，也不能为同一 pending 调用同时保留多个结果。

直接线性化点证明再为 $\operatorname{complete}(H')$ 中的每个操作 $o$ 选择抽象生效事件 $\lambda(o)$ 。对原本已返回的操作，该事件位于实际调用与响应之间；对已经生效但尚未返回的 pending 操作，可以追加与已固定结果相符的响应，事件仍位于调用和这个追加响应之间。尚未证明发生抽象效果的 pending 操作可以删去，却不能仅为凑出合法顺序而虚构效果。

按这些事件在执行中的先后得到全序 $<_{\lambda}$ ，必须满足两项责任：该顺序执行是顺序对象规格的合法历史；若 $o_1$ 的返回先于 $o_2$ 的调用，则 $o_1<_{\lambda}o_2$ 。这正是线性一致性的实时顺序要求，而非只保持每线程程序次序。

状态式证明通常扩充 pending-operation ghost state，并维护具体表示与抽象对象状态的关系。调用登记参数和未完成操作；普通内部步保持抽象状态不变；选定的线性化步骤执行恰好一个合法抽象操作并固定其结果；返回事件必须与已固定结果一致。由此得到从具体对象到原子规格的并发程序精化：每条具体调用—返回历史都有一个合法抽象顺序见证。

表示关系还必须满足干扰自由。本线程在某个控制点建立的“候选值尚有效”或“操作尚未线性化”等断言，要经其他线程所有可能的非线性化步骤保持，或在被破坏时让当前线程转入重试。只沿单线程代码画一个点，不能证明所有交错。

直觉

实现中的一次方法调用可能执行许多读、比较和重试；客户只需要相信它仿佛在区间内某一瞬间原子发生。线性化证明要找的不是最显眼的指令，而是第一次让抽象效果不可撤销、并能解释返回值的事件。此前步骤可以准备，之后步骤可以清理，但都不能改变已经确定的抽象历史。

重叠操作可按规格和实际返回灵活排序，非重叠操作却被墙钟区间强制排序。线性化点必须落在调用和返回之间，正好把这两类约束统一起来。点可能由帮助线程执行，也可能取决于未来选择，所以“每个方法固定一行代码”只是常见充分模式，不是定义。

例子与边界

考虑以 CAS 实现的 fetch_inc：

text

repeat
    old := load(c)
until CAS(c, old, old + 1)
return old

抽象规格在计数器值为 $n$ 时原子返回 $n$ 并把状态改成 $n+1$ 。失败 CAS 没有改变 $c$ ，可作为抽象停顿；成功 CAS 的比较保证成功前具体值正是 old，该步同时不可撤销地更新为 old+1，因此可匹配一次抽象 fetch_inc 并固定返回 old。成功步发生在调用之后、返回之前，满足区间条件。

最初的 load 不能作为线性化点。线程 A 读到 $4$ 后，线程 B 可能先成功把计数器改为 $5$ ；A 的 CAS 随后失败并重读。若在第一次 load 就把 A 抽象线性化为返回 $4$ ，便会制造两个操作都返回 $4$ 的非法顺序。重试分支正是其他线程干扰候选断言后的恢复路径。

这个证明假设 CAS 与计数器访问符合所声明的内存序。对指针结构，节点回收还可能引入 ABA：地址值恢复相同不代表抽象节点未变。直接点法也不适合所有算法；帮助机制中一个线程可以线性化另一线程的操作，未来依赖队列甚至需要模拟、后向推理或预言变量。无论方法如何，线性一致性仍是安全性质，不证明 CAS 循环最终成功或达到 wait-free 进展。

推论与应用

固定线性化点使证明可以按代码事件局部组织：非关键步骤证明表示不变式保持，关键原子步骤证明抽象状态转换，返回步骤核对结果。ghost history 可以记录已提交操作，帮助把具体状态与顺序规格联系起来；并发分离逻辑则可控制关键步骤所需的资源和抽象权限。

若找不到固定点，线性一致性的模拟证明可直接比较具体与抽象转移系统。模型检查也能在有限实例上搜索历史反例，但边界内没有反例不是参数化证明。实际审核还应分别核对 pending 调用 completion、异常或取消操作，以及每种方法的顺序规格，而不是只检查共享数据最终值。

参考资料

Maurice P. Herlihy and Jeannette M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects,” ACM TOPLAS 12(3), 1990, pp. 463–492。
Viktor Vafeiadis, “Automatically Proving Linearizability,” CAV, 2010, pp. 450–464。
Brijesh Dongol and John Derrick, “Verifying Linearisability: A Comparative Survey,” ACM Computing Surveys 48(2), 2015, Article 19。
Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, revised 1st ed., Morgan Kaufmann, 2012, Ch. 3。

形式陈述 ​

反向链接

形式陈述