线性一致性

线性一致性把每段有持续时间的调用压成一个点，同时保留客户端已经能够观察到的先后事实。实现内部可以有锁、CAS 重试、复制延迟与帮助步骤；只要每段可见历史都能压到合法顺序对象上，调用者便可按原子对象推理。

实时约束只比较不重叠区间，不要求物理时钟同步，也不要求副本同一纳秒更新。一个慢副本可稍后追上，只要系统不向客户端返回无法嵌入单一实时顺序的结果。

初值为 $0$ 的寄存器上，write(1) 完成后 read() 才开始，则读必须返回 $1$；把读排在写前会违反 ${<}_H$。若读写区间重叠，返回 $0$ 可把读线性化在写前，返回 $1$ 可放在写后，两种历史都可能合法。

队列给出更强的返回值约束。若 enqueue(a) 与 enqueue(b) 重叠，随后在二者都完成后调用两次 dequeue()，可以返回 $a,b$ 或 $b,a$；选定第一个返回值后，两次入队的线性顺序也随之确定。若第一次出队返回未曾入队的 $c$，无论如何移动线性化点都无法满足顺序队列规格。

Pending 调用不能一律删除：它可能已经改变对象并被其他完成操作观察到，此时 completion 应为它补响应；若尚未产生可见效果，才可删除。超时 API 还要说明“客户端停止等待”是否取消操作，否则稍后生效的写可能完全符合对象历史，却违背调用者误设的取消语义。

线性一致性是安全性质，不保证任何操作最终返回。一个永远悬挂的实现可能让所有已完成操作都合法，却没有 wait-free、lock-free 或阻塞进展。

线性一致性具有局部性：若每个对象投影都有合法线性化，则可把这些顺序与全局实时偏序合并成组合历史的线性化。证明骨架利用每个对象顺序都已保持自身实时边；若合并关系有环，沿环必能推出某个操作在真实时间上先于自身。顺序一致性公理库顺序一致性Sequential consistency共享内存中的读写操作可排成保持各线程程序顺序并解释所有读值的单一全序。没有这项逐对象可组合保证。

任何线性一致历史也满足同一对象规格下的 SC，因为它的全序公理库全序Total order · Linear order任意两个元素都可比较的偏序。保留了更强的实时顺序，当然也保留每进程顺序。因此本页性质是 SC 的特例；反例是写已完成后另一客户端才读旧值，它可满足 SC，却不线性一致。

语言或硬件的内存一致性模型公理库内存一致性模型Memory consistency model · Memory model规定并发程序的内存操作可以产生哪些可观察执行的契约。约束更细粒度的读写事件。并发队列、寄存器与复制存储常把线性一致性作为外部语义；状态机复制还需一致日志、确定性执行、响应时机和客户端去重，才能从内部提交推出端到端历史条件。

证明实现线性一致时，可把内部执行路径公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。投影成调用/返回历史，再建立到顺序对象的精化或模拟关系公理库系统精化关系Refinement relation · System refinement · Specification refinement以行为包含、模拟或表示映射约束实现，使其允许行为不超出规格。。成功证明给出每段并发历史的合法顺序见证；模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。失败则应返回具体历史及无法满足实时顺序和返回值约束的反例。这里验证的是历史级安全性质，不把内部每一步强行与抽象操作一一对应，也不顺带证明进展。