正式的Linux内核内存模型

Question

图像和引用来自: 可怕的小孩子和令人不安的成年人:Linux内核中的并发

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

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是

{(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)}.