如何理解“正式内核内存排序模型”中的 limus 测试 #5？

Question

在文章“A formal kernel memory-ordering model”中，提出了以下违反直觉的记忆模型试金石：

P0(int *a, int *b)
{
  WRITE_ONCE(*a, 1);    //1
  smp_wmb();
  WRITE_ONCE(*b, 1);    //2
}

P1(int *a, int *b)
{
  int r1;

  WRITE_ONCE(*b, 2);    //3
  smp_mb();
  r1 = READ_ONCE(*a);   //4
}

exists
(b=2 /\ 1:r1=0)

观察b == 2 暗示 3) 在 2) 之后完成。并且由于 2) 是在 1) 之后排序的，因此观察 r1 == 0 永远不可能。给出的解释是对b == 2 的观察并不意味着 3) 是在 2) 之后排序的。相反，一个 hart 较早发出的内存写入可能会覆盖另一个 hart 稍后发出的内存写入。 this presentation 的第 71-72 页显示了一种可能发生这种情况的机制。

这真的发生在当前的硬件中吗？例如，RISC-V 在其specification（第 88 页）中有以下“加载值公理”：

每次加载的每个字节i返回由以下存储中全局内存顺序最新的存储写入该字节的值：

1. 在全局内存顺序中写入该字节并在 i 之前的存储

2. 写入该字节并且在程序顺序中位于 i 之前的存储

这是否禁止观察到较早的写入可以覆盖以后的写入？

Answer 1

经过大量阅读，这是我目前对问题的理解。

与 RISC-V 的 RVWMO 模型不同，Linux 内核的强模型包含了“写传播”的概念。强模型定义指出：（强调我的）

当 CPU 提交对指定目标地址的读取请求时， 内存子系统找到最新的写入（在目标地址的 coherence order) 已传播到 CPU 并返回值 由该写入存储。

这与 RVWMO 的加载值公理形成对比，RVWMO 的内存只是按全局内存顺序返回最新的写入。换句话说，RVWMO 假设每次内存写入都会立即同时传播到所有 CPU。

相应地，smp_wmb() 和smp_mb() 之间存在显着差异。 smp_wmb() 是一个弱屏障，而smp_mb() 是一个强屏障。弱屏障只是告诉内存在屏障之后的写入应该始终在屏障之前的所有写入之后传播。一个强大的屏障实际上会等到之前的写入已经传播到所有 CPU 和“相干点”。

以下是我对试金石测试期间发生的情况的想法：

1. P0 将两次写入和屏障发送到内存。然后它们传播到相干点，但没有到达 P1。
2. P1 将写入发送到内存并等待直到它传播到 P0。在此期间，P0 的写入均未到达 P1。因为P1的写入比P0的写入到相干点晚，所以b的最终值为2。
3. P1 读取变量a。因为P0的写还没有到P1，所以得到了初始值0。
4. 来自 P0 的写入最终到达 P1。但是，P1 永远不会看到 b == 1，因为 WRITE_ONCE(*b, 2); 以一致性顺序出现在后面。

现在为什么用smp_mb() 替换smp_wmb() 会消除观察到的结果？因为在这种情况下，P0 实际上会等到它的第一次写入传播到 P1，然后再发送它的第二次写入。现在r1 == 0 暗示 P0 中的屏障仍未完成，但 P1 中的屏障确保 P1 中的写入已到达所有 CPU 和相干点。因此，P0 中的第二次写入必须晚于 P1 中的写入到达相干点。因此我们不能有b == 2。