正式 Linux 内核内存模型

Question

图片和引用来自： Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel

让我们考虑一个简单的程序：

cumul-fence 定义为：

cumul-fence := A-cumul(strong-fence ∪ po-rel) ∪ wmb
A-cumul(r)  := rfe';r

在 3.2.3 的链接出版物中写道 (b, e) ∈ prop。由此我们可以得出结论 (c, d) ∈ cumul-fence。

所以，让我们看看：

po-rel = {(c,d)}
strong-fence = {(a,b),(e,f)}
wmb = {}
rfe = {(d,e)}
rfe' = {(d,d), (d,e), (e,e)} <- reflexive closure of rfe. 
A-cumul({(a,b),(e,f),(c,d)}) = {(d,d), (d,e), (e,e)};{(a,b),(e,f),(c,d)} = {(d,f), (e,f)}
cumul-fence = {(d,f), (e,f)}

所以，我们可以看到 (c,d) 不在 cumul-fence 中。有人可以解释一下我的推理哪里不正确吗？

Answer 1

rfe'，rfe的reflexive closure，是

{(d,e), (a, a), (b, b), (c, c), (d, d), (e, e), (f, f), (k, k), (r, r)}

因为节点集是 {a, b, c, d, e, f, k, r}。

从那里，cumul-fence 是 {(d, f), (a, b), (c, d), (e, f)}。

正式 Linux 内核内存模型

Formal Linux Kernel Memory Model

x86

memory-model

linux-kernel