并发程序精化

精化不是比较两份代码“看起来是否相似”，而是给观察者设一场辨认测试。若任何许可客户看到实现产生的一段行为，都能在规格世界找到相同观察，那么客户不能用契约允许的手段证明实现越界。内部多走几步、改变表示或固定某个合法选择都可以被隐藏。

客户集合和观察接口不可省略。锁内暂时破坏的数据关系，对只能经锁访问的客户可能完全不可见；同一实现面对能无锁读取内部字段的监控线程却可能泄露中间状态。所谓“实现精化规格”总是相对于谁能看、能看见什么以及调度允许什么。

抽象对象提供原子 swap(x,y)，从状态 $(1,2)$ 一步转到 $(2,1)$。具体实现取得同时保护两格的排他锁后执行

t := x
x := y
y := t

内部状态轨迹经过 $(1,2)\to (2,2)\to (2,1)$。若 $\mathcal{K}$ 中所有客户只能通过同一把锁保护的 API 观察这两个值，$(2,2)$ 属于隐藏的内部状态；调用前后的可见行为与抽象原子 swap 匹配，因而这段实现可以精化抽象规格。

若加入一个不取锁的 metrics 线程，它可能在两次写之间读到 $(2,2)$。抽象 swap 的任何轨迹都没有这个可见状态，于是存在具体行为找不到抽象见证，包含失败。修补证明不能只把该读取标成内部事件，因为它已进入客户观察；必须收紧客户契约、改变实现原子性或扩大规格允许行为。

只比较有限安全前缀还可能容忍无限内部循环：每个已经产生的可见前缀都合法，实现却永不返回。要保存终止、无饥饿或公平活性，需采用 divergence-sensitive 行为和对应调度假设。弱内存下，编译器与硬件还可能暴露顺序语义中不存在的读写观察，除非精化模型明确包含内存排序。

线性一致性公理库线性一致性Linearizability每次操作可放置在调用与返回之间的单点，使历史等价于满足实时顺序的顺序规范。可把并发对象的每段历史匹配到尊重实时顺序的原子顺序规格，因此在合适客户和内存模型下提供强有力的对象精化原则。它仍只约束安全历史；从线性一致性自动推出 contextual refinement 往往还需要客户数据竞争自由、调用接口封装和异常语义等条件。

并发精化支持逐层开发：无锁实现精化原子对象，原子对象再精化业务规格；每层隐藏不同内部事件。传递性要求各层观察字母表和发散约定兼容。若中间层把一个上层可见失败悄悄隐藏，简单套用集合包含并不能得到端到端结论。