代码之家 › 专栏 › 技术社区 › Gilgamesz

正式的Linux内核内存模型

memory-model x86 linux-kernel

5

Gilgamesz · 技术社区 · 5 年前

图片和引文来自: 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) 不在 堆积篱笆 . 有人能解释我的推理哪里不对吗?

1 回复 | 直到 5 年前

1

Margaret Bloom 5 年前

rfe' , the reflexive closure 属于 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)} .