缓存一致性性的 实现等价
这里 讲述了 缓存一致性的 形式化定义 . 是从 高层次 形式化定义了 缓存一致性 , 但是没提 如何实现 .
那么从实现角度考虑的话, 即 实现了什么就能满足缓存一致性
- A 缓存一致性的实现 等价条件(操作机制,即实现角度)
A1.写传播将一个高速缓存中的修改传播到其他高速缓存中
A2.事务串行化对同一个地址的读写事务,被所有CPU串行化看到
- B 缓存一致性的 形式化定义(形式化角度)
B1. 读 返回最近写
B2. 保持该处理器本身的发出顺序同时形式化定义中推导出了 write串行化
- 两者 整体关系
这两个观点本质上是等价的,它们确实是从两个不同的角度对“缓存一致性”进行了充分必要性的刻画。
观点A 这是从系统实现机制的角度,描述实现一致性所必须满足的两大行为要求。
观点B 这是从数学建模或行为观察的角度,用序列和返回值的规则来定义一致性行为。✅ 形式化定义中的**“构造序列 + 顺序保持 + 读返回最近写”,等价于机制角度的“写传播 + 事务串行化”**。
“它们好像不一样,但是又等价,都描述了缓存一致性的充分必要条件,是从不同角度切入。”
观点A更适合工程师在“设计协议”时思考;
观点B更适合做“理论验证”时使用。
两者互为支撑、互相印证。
比较点 | 观点A(机制) | 观点B(形式化序列) | 等价说明 |
---|---|---|---|
写传播 | 写能传播给其他处理器 | 序列中每个写都能影响到后面的读 | 写传播确保写入值可见 |
事务串行化 | 所有读写可线性化,读返回最近写 | 构造一个满足“读返回之前最近写”的序列 | 二者等价,都是全序一致性 |
保持程序顺序 | 隐含包含(事务串行化要保证原子性) | 明确要求处理器自己的顺序不能乱 | 体现为“顺序保持性” |
针对每个地址 | 是,事务串行化强调的是单地址行为 | 是,形式化也是对每个地址构造一个序列 | 聚焦相同地址,模型一致 |
视角 | 类比描述 |
---|---|
机制角度(观点A) | 就像是在设计一个机器,列出它必须具备哪些功能部件:你需要“广播写的结果”(写传播)和“安排执行顺序”(事务串行化)。 |
数学定义角度(观点B) | 像是在做形式化验证:你只需要构造一个“解释行为”的读写序列,满足某些逻辑关系。 |
- 两者中局部的关系
A1 是 B1 的 必要非充分条件 // A1 是方法, 通过A1 可以实现B1
A2 和 B2 关注的角度不同,一个跨处理器(A2) , 一个局部处理器(B2) , 不是谁等级更高,只是面向不同纬度write串行化 是 事务串行化 的必要非充分条件