线性一致性的模拟证明

前向模拟像同步播放两段录像：实现每走一步，证明者立即决定抽象机如何跟随。固定或由过去决定的线性化点很适合这种方式。若当前具体状态允许多个抽象解释，而正确解释要等未来某次 dequeue 返回后才知道，立即选择可能过早；后向模拟从已经显露结果的后态向前安排抽象见证。

两种方向最终都服务于同一个行为包含结论，却不是无条件可互换的语法技巧。前向关系易按实现步骤归纳，但可能因未来依赖而不存在；后向关系能保留一组尚未决定的抽象顺序，证明义务和有限分支、停顿条件也更细致。

Treiber 栈用 top 指向单链表。取关系 $R$：从具体 top 可达的节点值序列恰等于抽象栈序列，另有 ghost 状态记录每个 pending 方法。push(v) 先分配节点并设置 next，这些线程局部步骤在抽象侧停顿；成功把 top 从旧头 CAS 为新节点时，关系要求抽象执行一次 push(v)。失败 CAS 不改共享链，抽象仍停顿并让线程重试。

pop 读取头和 next 也可停顿；成功 CAS 移除头时匹配一次抽象 pop，并固定返回被移除节点的值。若初始具体链为 $[b,a]$，成功 pop 后为 $[a]$，抽象序列同步从 $[b,a]$ 变 $[a]$ 并返回 $b$，关系可直接复算。

该关系假设节点在仍可能被其他线程引用时不会释放并复用。若地址经历 ABA，CAS 可能成功但“同一地址”代表不同逻辑节点，简单可达链关系不再保持；必须加入 hazard pointer、epoch 或带版本指针的回收证明。对无限内部重试，零步抽象匹配足以证明有限历史安全，却不能证明活性；divergence-sensitive 精化需正步进展或良基停顿度量。

一般系统上的一条局部反向条件也不自动给 trace inclusion。Schellhorn、Derrick 与 Wehrheim 的完备性结果针对合适的 canonical linearizability specification 及其技术条件；不能改写成“任意两个 LTS 的后向模拟都无条件完备”。同样，编译器文献可能采用相反的 source/target 命名，必须从本页的具体到抽象匹配式重新判断方向。

模拟把线性化点证明推广为状态关系证明：成功原子步可匹配抽象操作，帮助步骤可以更新别人的 pending ghost，未来依赖算法则用后向关系或辅助变量延迟选择。关系还可机械化为定理证明器中的归纳或共归纳义务，并与对象表示不变式组合。

抽象系统的设计决定证明是否诚实。若它额外允许不尊重实时顺序的调用返回，模拟成功也不能推出线性一致性；若它遗漏合法 pending completion，证明又可能无谓失败。因此必须先证明抽象 LTS 的可见 histories 与历史定义一致，再把模拟定理接上，而不是用“原子规格”四个字代替这一接口。