基于SC内存一致性模型两个核心约束的放松维度
文章目录
- 两个放松维度
- ✅ 基础回顾：SC 两大核心约束
- ✅ 针对 **核心约束 1（程序顺序）** 的放松维度
- 1.1 指令对顺序放松（Memory Order Relaxation）
- 1.2 地址相关性分类
- ✅ 针对 **核心约束 2（操作原子性）** 的放松维度
- ✅ 总结结构图（思维导图形式）
- ✅ 小结
- 除了 SC 以外，其他所有一致性模型，**本质上都是对 SC 的放松（relax）**。
- ✅ 你提到的 Wikipedia 内容回顾
- ✅ 你的观点：
- ✅ 我的明确回应：
- 🔹 学术支持来源：
- 🧠 但为什么不是所有文献都明确说“其他模型是 SC 的放松”？
- 1. **表达方式不同（构造 vs 公理）**
- 2. **不是每种模型都能从 SC 形式化变换一步得到**
- ✅ 最后简洁总结
现在是在从理论模型的角度系统性地分析内存一致性模型的 可放松维度，这是理解一致性模型非常本质也非常精确的方法。
你已经提出了一个非常清晰的分类框架。我们就从你这两个核心约束出发，来系统总结有哪些 relaxation 方向。
两个放松维度
✅ 基础回顾：SC 两大核心约束
| 编号 | 核心约束 | 描述 |
|---|---|---|
| 1 | 程序顺序必须保留（Preserved Program Order） | 每个处理器的内存访问必须按程序顺序出现在全局序列中 |
| 2 | 操作原子性（实际上是指write atomicity） | 所有处理器(包括自身处理器)对 store 的观察必须一致（即：写是同时对所有处理器可见的） |
✅ 针对 核心约束 1（程序顺序） 的放松维度
主要是探讨哪些 指令对 可以在执行上不遵守程序顺序：
1.1 指令对顺序放松（Memory Order Relaxation）
注意：放松主要发生在不同地址之间，相同地址往往被限制（除非特别说明）
针对某种类型 放松后 , 即 每个处理器的 此种类型 内存访问 不必 按程序顺序出现在全局序列中
| 放松类型 | 示例 | 描述 |
|---|---|---|
| Load → Load | load a; load b | 允许后发出的读先执行（并返回较新值） |
| Load → Store | load a; store b | 允许写早于读完成 |
| Store → Store | store a; store b | 允许乱序提交多个写 |
| Store → Load | store a; load b | 允许读早于写完成，是最典型也最常被单独分类放松的一种 |
| Dependency Load | r1 = load a; r2 = load r1 | 允许对地址依赖也乱序（例如 RISC-V 就默认支持） |
1.2 地址相关性分类
对于上面每一种顺序，还可以进一步细分：
| 地址关系 | 含义 |
|---|---|
| 同地址（same address） | 比如 store a; load a —— 必须严格约束，大多数模型不允许放松 |
| 不同地址（different address） | 比如 store a; load b —— 是各种 relax 的重点 |
✅ 针对 核心约束 2（操作原子性） 的放松维度
这里我们探讨写的可见性是否原子，涉及“谁能读到谁的写”：
| 放松类型 | 描述 | 说明 |
|---|---|---|
| Can Read Own Write Early (CROWE) | 处理器可以在写操作尚未对所有处理器可见之前，自己先读到自己的写 | 很多模型允许，比如 TSO、ARM、RC |
| Can Read Others’ Write Early (CROWE-O) | 处理器可以在写未对所有处理器可见之前，读到别人的写 | 会打破写的原子性，更激进 |
✅ 总结结构图（思维导图形式）
针对SC核心约束1的relax
Preserved Program Order
├── Relax Load → Load
├── Relax Load → Store
├── Relax Store → Store
├── Relax Store → Load
└── Relax Dependency (address dep.)每种顺序还细分为：├── 相同地址（通常不允许放松）└── 不同地址（放松的主要目标）针对SC核心约束2的relax
Atomic Visibility
├── Can Read Own Write Early
└── Can Read Others’ Write Early
✅ 小结
这个理论框架可以用来分析任何内存模型，只要明确它对每一种放松的支持情况。
| 模型 | Relax Store→Load | Relax Load→Load | CROWE | CROWE-O |
|---|---|---|---|---|
| SC | ❌ 不允许 | ❌ 不允许 | ❌ 不允许 | ❌ 不允许 |
| PC | ✅ 不同地址可放松 | ❌ | ✅ | ❌ |
| RC | ✅ | ✅ | ✅ | ✅ |
| ARM | ✅ | ✅ | ✅ | ✅ |
除了 SC 以外，其他所有一致性模型，本质上都是对 SC 的放松（relax）。
你的理解在理论上是正确的，也已经和主流一致性模型的学术表达基本一致。我们来分层确认和解释你的观点。
✅ 你提到的 Wikipedia 内容回顾
你引用的是 Consistency model – Wikipedia 页面中“Relaxed memory consistency models”章节中的这段：
One way to categorize the relaxed consistency is to define which sequential consistency requirements are relaxed. We can have less strict models by relaxing either program order or write atomicity requirements defined by Adve and Gharachorloo, 1996.
…
In the relaxed write atomicity model, a process can view its own writes before any other processors.
这明确指出：
Relaxed consistency models 是通过放松 SC 的约束得到的。
✅ 你的观点：
我认为除了 SC 以外，其他所有一致性模型，本质上都是对 SC 的放松（relax）。
✅ 我的明确回应：
✔️ 你说得是对的，这就是一致性模型的“形式化语义谱系”主流观点。
在学术文献和架构理论中，这种说法被称为：
SC as the base model; other models as systematic relaxations.
🔹 学术支持来源：
-
Adve & Gharachorloo 1996 的经典论文《Shared Memory Consistency Models: A Tutorial》正是这样分类的；
-
所有主流模型（TSO、PSO、RC、WO、Alpha、ARMv7）都可以看作是：
SC − 某些顺序保证 − 写的原子性保证
🧠 但为什么不是所有文献都明确说“其他模型是 SC 的放松”？
有两个原因：
1. 表达方式不同（构造 vs 公理）
一些架构手册（如 ARM、RISC-V）会直接以操作语义构造内存模型，而不再溯源于 SC。这是实用导向。
但从 理论角度（如你引用的 Wikipedia 段落），一致性模型确实是：
“在 SC 的基础上，通过系统性地 relax 某些约束而得到的”
2. 不是每种模型都能从 SC 形式化变换一步得到
例如一些特定的 relaxed 模型（如 lazy release consistency）在实现或缓存交互上引入了更多机制，不容易形式上“从 SC 扣除一条规则”得到。但在概念上，它仍是“SC 的子集行为”。
✅ 最后简洁总结
| 观点 | 是否正确 | 说明 |
|---|---|---|
| 除 SC 外的模型都是 SC 的 relax | ✅ 是的 | 这是理论上主流的理解方式 |
| 为什么文档中有时不强调这一点？ | ✅ 因为实现/表达角度不同 | 工程文档通常更关注行为规范而非语义来源 |