顺序一致性 | Codeboy's Blog

形式陈述

本页专指 Lamport 的共享内存顺序一致性，它是内存一致性模型的一种。设执行的内存操作集合为 $E$ ，每个线程给出程序顺序 $<_{\mathrm{po}}$ 。执行是顺序一致的，当且仅当存在 $E$ 上的全序 $<_{S}$ ，满足：

<_{\mathrm{po}}\ \subseteq\ <_S,

并且每次读 $r=R(x)\Rightarrow v$ 返回 $<_S$ 中位于 $r$ 之前、对位置 $x$ 的最后一次写所写的值；若没有这样的写，则返回 $x$ 的初值。全序 $<_S$ 是一次执行的见证，不要求实现真的由单一中央调度器逐步运行。

定义只保留每线程程序顺序。若一个线程的操作已经响应、另一线程之后才发起操作，跨线程的这段实时先后仍不必进入 $<_S$ ；这正是它与线性一致性的量词差异。

直觉

SC 允许把并发执行解释成某一种合法交错。每个线程都看见自己的指令按程序次序发生，所有线程还必须共享同一解释；自由度只在不同线程操作如何穿插。它比“各地址各有一个写序”更强，因为跨地址读值也必须同时嵌入同一个全序。

这个心智模型不携带墙上时钟。不同线程的两个非重叠操作仍可在见证全序中反向排列，只要各自线程内没有约束被破坏。

例子与边界

初值 $x=y=0$ ，线程 $P$ 执行 $W(x,1);R(y)\Rightarrow0$ ，线程 $Q$ 执行 $W(y,1);R(x)\Rightarrow0$ 。若存在 SC 见证，则程序顺序与读初值依次给出

W(x,1)<_S R(y)<_S W(y,1)<_S R(x)<_S W(x,1),

形成严格全序中的环，故该结果不可能是 SC。

这个例子还展示 SC 不具对象局部可组合性。单看寄存器 $x$ ，可把 $R(x)$ 排在 $W(x,1)$ 前；单看 $y$ 也可作同样排列，所以两个对象投影分别满足 SC。合并后却出现上述环。线性一致性具有局部性：逐对象证明可组合成全局证明，这是两种条件在模块化上的另一处差异。

另一方面，若客户端 $A$ 的 write(1) 已经返回，客户端 $B$ 之后才调用 read() 却读到旧值 $0$ ，只要两个客户端各自没有别的顺序约束，仍可在 $<_S$ 中把读排到写前，因此可能满足 SC；它违反线性一致性的实时顺序。

“所有处理器最终看到相同值”只是收敛性，不等同于存在统一操作序。SC 也只是一项安全约束，不承诺某次读写最终执行、锁不会饥饿或副本在故障后仍可用。

推论与应用

SC 是弱内存研究的基准，却不是现代语言与硬件的默认行为。特定语言的 SC-for-DRF 保证只在程序消除模型所定义的数据竞争，并正确使用同步与原子内存序时，才把相应观察映射回某类 SC 交错。

对同一个顺序对象规格，任何线性一致历史都能提供一个保程序顺序的 SC 见证，反向不成立。这个子类关系不抹平抽象层：SC 常约束内存操作集合，线性一致性常约束调用—响应区间。应用结论前仍要确认两者排列的是同一批操作。

验证工具可从程序的执行轨迹提取内存事件，再由模型检查寻找无法嵌入任何保程序序全序的反例。工具探索哪些 interleaving 取决于语言和硬件模型；SC 的定义本身并不保证实现允许所有交错，也不保证只允许 SC 交错。

参考资料

Leslie Lamport, “How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs,” IEEE Transactions on Computers C-28(9), 1979, pp. 690–691，Full paper。
Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012，Ch. 3。