缓存一致性的单块契约

想象每块有一支可转交的写笔。拿到写笔的人才能改，别人不能同时把旧副本当有效读值。但只把笔交过去、忘了交最新纸张仍会出错，所以权限交接必须伴随数据交接。

各副本不必每一时刻都存着相同字节。被标为无效的旧副本可以仍占着物理空间，只要不被当成合法命中使用。内存也不是永远唯一的最新来源。

权限对，数据仍可能错 ​

初始x=0，P取得独占权限并写x=1，内存仍为0。随后P失效，Q成为唯一写者；如果Q从旧内存取0再执行“加一”，得到1，而不是应有的2。任一时刻只有一个写者，权限检查通过，数据值不变量却被破坏。

修复不是“再加一个独占位”，而是要求P在交接时供出含1的最新副本，或先回写到可信的下层，再让Q取得数据。

单地址规则不能排除双零 ​

P执行 W(x,1); R(y)，Q执行 W(y,1); R(x)。若各自的写先停在本地写缓冲，两个读都可在对方写传播前取得初值0；随后两次写再分别进入各地址的coherence次序。每个地址都可以有合法写序，这仍不能推出跨地址的顺序一致性。

内存一致性模型理路内存一致性模型Memory consistency model · Memory model规定并发程序的内存操作可以产生哪些可观察执行的契约。决定这种双零观察是否允许，以及哪些栅栏能排除它。本页不再重建已有的x86-TSO轨迹，也不把coherence当作SC的别名。

回写到DRAM仍可能断电丢失 ​

一个块已经完成权限交接，所有合法读都看到1，甚至内存副本也为1；若所有副本都位于易失介质，断电仍可全部丢失。coherence约束运行中的读写，持久化约束故障后哪些写存活。两项义务不能用同一个“已一致”状态代替。

验证协议要同时查权限不变量和数据不变量，还要另查请求是否最终完成。永远不授予写权限的机器可能满足安全条件，却不能提供有用进展。

协议通常按整个缓存行管理权限，因而不同变量落在同一行也会互相干扰；这形成伪共享理路伪共享与缓存行粒度False sharing · Cache-line ping-pong用不同变量共享一条缓存行的写权限往返解释伪共享，并复算隔离布局前后的事务数。。它说明权限粒度会影响传输，即使程序变量之间没有读写依赖。