Formal Linux Kernel Memory Model

Question

images and citations comes from: Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel

Let's consider a simple program:

cumul-fence is defined as:

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

In the linked publication in 3.2.3 it is written that (b, e) ∈ prop. From that we can conclude that (c, d) ∈ cumul-fence.

So, let's see:

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)}

so, as we can see (c,d) is not in cumul-fence. Can someone explain me where my reasoning is incorrect?

Answer 1

rfe', the reflexive closure of rfe, is

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

since the set of nodes is {a, b, c, d, e, f, k, r}.

From there, cumul-fence is {(d, f), (a, b), (c, d), (e, f)}.