顺序一致性

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

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

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

形成严格全序中的环，故该结果不可能是 SC。内存一致性模型公理库内存一致性模型Memory consistency model · Memory model规定并发程序的内存操作可以产生哪些可观察执行的契约。页给出 2010 x86-TSO 下缓冲两次写、再读两个初值的完整执行，并证明在两个线程的写与读之间分别加入 MFENCE 后如何排除它。允许性需要一条模型内执行，禁止性则需要对所有候选次序的约束论证。

这个例子还展示 SC 不具对象局部可组合性。单看寄存器 $x$，可把 $R(x)$ 排在 $W(x,1)$ 前；单看 $y$ 也可作同样排列，所以两个对象投影分别满足 SC。合并后却出现上述环。线性一致性公理库线性一致性Linearizability每次操作可放置在调用与返回之间的单点，使历史等价于满足实时顺序的顺序规范。具有局部性：逐对象证明可组合成全局证明，这是两种条件在模块化上的另一处差异。

一般对象的区别也可以直接看到。初始空队列中，A 的 enqueue(a) 已返回，B 才执行并完成 enqueue(b)，随后 B 的 dequeue() 返回 b。按 B 入队、B 出队、A 入队排列，是保持各进程投影的合法 FIFO 顺序，所以这个历史满足 SC；线性一致性却必须保留 A 先完成的实时顺序，因此应先弹出 a。

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

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

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

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

验证工具可从程序的执行轨迹公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。提取内存事件，再由模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。寻找无法嵌入任何保程序序全序的反例。工具探索哪些 interleaving 取决于语言和硬件模型；SC 的定义本身并不保证实现允许所有交错，也不保证只允许 SC 交错。