linearizability · 三级进展保证

正确性判据与进展保证

单线程的数据结构有唯一正确答案：给定一串操作，结果是确定的，测试只需比对这个答案。多线程一进来这个前提就没了。两个线程同时对同一个栈做 push，谁的元素在上面不由代码决定，两种结果都对。测试因此不能再问「结果对不对」，只能问「这个结果讲不讲得通」。

本页立两把尺子。一把量正确性，一把量效率，两把互不替代：一个结构可以完全正确却毫无进展保证，也可以进展保证很强而吞吐很差。

1 · 同一段程序的多种合法结果

场景固定为两个线程各做一次 push 再各做一次 pop，栈是 Treiber 栈（实现见 Treiber 栈与内存回收 §1）。把每条原子指令当作不可分割的一步，模拟器穷举出这些指令的全部交错，共 2114 条。

2114 条交错在外部只呈现 12 种不同的观察结果。差别被吸收掉了：多数交错的区别只在某次 CAS 失败重试了几轮，重试对调用方不可见。这 12 种里包含 T1.pop → 2 这类看着奇怪的结果，即 T1 弹出的是 T2 压进去的元素。

图 1-1 · 两线程各 push 加 pop 的全部交错按可观察结果归类，甘特条是各操作的调用与返回区间，黑点是检查器安排的线性化点。可切换操作集与结果，也可把最后一个返回值篡改成 99 观察检查器判否。

同一个操作集换成 T1 做 push 加 pop、T2 只做一次 push，交错数降到 53，可观察结果降到 6 种。规模稍减，穷举的代价就掉一个量级，这是本系列反复利用的一点。

2 · linearizability

定义 2.1（linearizability） 一次并发执行是可线性化的，当且仅当存在一个把全部操作排成一列的顺序 $\sigma$ ，同时满足两条： $\sigma$ 能被该对象的顺序规格解释，即按 $\sigma$ 逐个执行时每个操作的返回值与实际观察到的一致；并且 $\sigma$ 与实时序相容，即若操作 $a$ 的返回早于操作 $b$ 的调用，则 $a$ 在 $\sigma$ 中排在 $b$ 之前。

等价的说法是每个操作都有一个 linearization point，是它的调用与返回之间的某个瞬间，操作在那一瞬间原子生效。两种说法互推：给定顺序 $\sigma$ 可以在各操作的区间里挑出一列递增的瞬间，反之给定一列瞬间按大小排序即得 $\sigma$ 。

这个定义的力量在于它是局部的：若干个各自可线性化的对象组合在一起，整体仍可线性化。serializability 没有这条性质，这也是数据库事务与并发对象用两套判据的原因。

判定算法是搜索。反复挑一个「可以排第一」的未决操作，用顺序规格算出它应有的返回值，与实际观察到的比对，不符就回溯。可以排第一的判据是没有别的操作整体先于它，也就是它的调用步号不晚于所有未决操作里最早的那个返回步号。

3 · 区间约束与收尾状态

区间是唯一的硬约束。图 1-1 里 T1.pop → 2 之所以合法，是因为 T2 的 push 与 T1 的 pop 在时间上重叠：T2 的 CAS 已经换成功，T1 的 CAS 才发生。若 T2 的 push 完整地落在 T1 的 pop 结束之后，同样的返回值就立刻非法。

检查器另有一条容易被漏掉的收尾断言：顺序解释跑完之后，规格状态还要与结构的实际残留内容对上。少了这一条会漏掉一整类错误，即所有返回值都合法而结构内部已经烂掉。CAS 与 ABA §3 的 18 条反例全部属于这一类，只比对返回值的话检查器一条都抓不到。

警示 · 可线性化是关于一次执行的性质，不是关于程序的。一个有缺陷的实现在多数交错下都可线性化，缺陷只在少数交错上显形。本页的 Treiber 栈在 2114 条交错上全绿，而同一个引擎里那个用普通 store 链接节点的队列，20 条交错里有 18 条不可线性化。测试的价值来自穷举，不来自跑得多。

4 · 进展保证的三级

正确性之外的第二把尺子，与渐近复杂度无关。一把大锁护住的栈和 Treiber 栈都是 $O(1)$ 的 push，区别在于某个线程停住时会发生什么。

wait-free 每个线程在有界步数内完成自己的操作，与其他线程的行为无关<br> lock-free 总有某个线程在推进，但不保证是哪一个<br> obstruction-free 若从某刻起只让一个线程单独跑，它能在有界步数内完成

三级严格递强。fetch-and-add 实现的计数器是 wait-free：一条指令就是一次操作，任何交错下最坏步数恒为 1。load 加 CAS 循环的计数器只是 lock-free：CAS 失败意味着别人成功了，全局在推进，但某一个倒霉线程可能反复重试，实测两线程下最坏 4 步、三线程下最坏 6 步。自旋锁版本连 obstruction-free 都不是，持锁者一停，单独放任何一个别的线程跑都跑不出来。

图 4-1 · 四种计数器实现在全部交错下的单线程最坏步数与终值集合。可调线程数从 2 到 3，观察 CAS 循环的最坏步数随之上升而 FAA 恒为 1。

把「某个线程停住」做成实验，三级的差别一眼可辨。冻结一个线程之后另一个线程能否完成，是进展保证的操作性定义。

图 4-2 · 冻结 T1 于程序的某一步后，T2 能否完成以及要走多少步。可切换 Treiber 栈与自旋锁两种实现，并调整冻结位置。

实测：Treiber 栈在 push 的任意一步冻结 T1，T2 都在 5 步内跑完；自旋锁版本冻结在第 1、2 步时 T2 跑满 2000 步仍在自旋，那两个位置正好是「锁已拿到、尚未放开」。

5 · lock-free 与吞吐的关系

lock-free 保证的是没有线程能阻塞所有人，它不保证吞吐更高，这两件事常被混为一谈。

无竞争时，CAS 循环通常比加锁快，因为省掉了系统调用与上下文切换。高竞争时结论反过来： $n$ 个线程抢同一个 cell，每一轮只有一个 CAS 成功，其余 $n-1$ 次全部作废并且各自带走一次 cache line 往返。实测把 8 个线程压在单个分片上做 1600 次自增，CAS 失败 5600 次；换成一把互斥锁反而少做很多无用功，因为等锁的线程是睡着的，不占总线。

lock-free 真正买到的是尾延迟与故障容忍：没有优先级反转，没有「持锁线程被换出去导致全体停摆」，也没有「持锁线程崩溃导致结构永久锁死」。这几条在实时系统与内核里值钱，在批处理吞吐场景里未必。降低争用是另一条正交的路，见分片与争用。

注 · 本页开始前的猜想是「操作数加倍会让可观察结果爆炸，而结果一多总能撞上不可线性化的执行」。实测两条都不成立：2114 条交错只压出 12 种结果，且 168843 条交错的三操作版本同样一条反例都没有。正确实现就是不出反例，加大规模只是把机器跑热。反例必须来自故意做坏的实现，这一判断决定了本系列此后每一页都配一个坏版本。

6 · 参考文献

Herlihy, M. P., & Wing, J. M. (1990). Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3), 463–492.
Herlihy, M. (1991). Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 13(1), 124–149.
Herlihy, M., Luchangco, V., & Moir, M. (2003). Obstruction-free synchronization: double-ended queues as an example. Proceedings of the 23rd International Conference on Distributed Computing Systems, 522–529.
Wing, J. M., & Gong, C. (1993). Testing and verifying concurrent objects. Journal of Parallel and Distributed Computing, 17(1–2), 164–182. 本页检查器用的线性化搜索出自此文。