Формальная модель памяти ядра 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)}.