Re: Question about PB rule of LKMM

[Andrea Parri]

> > Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> > is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
> > 
> > The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
> > 
> >   [Marked]         ; (overwrite & ext)? ; cumul-fence*     ; [Marked]          ; rfe?            ; [Marked]
> >   (P0:Wx1, P0:Wx1)   (P0:Wx1, P1:Wx8)     (P1:Wx8, P1:Wx8)   (P1:Wx8, P1:Wx8))   (P1:Wx8, P0:Rx)   (P0:Rx, P0:Rx)
> > 
> 
> So the cumul-fence relation includes the same Store? This is hard to
> understand, because it is defined as:
> 
>   let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> 	po-unlock-lock-po) ; [Marked] ; rmw-sequence
> 
> There is at lease a rmw-sequence in the relation link.
> 
> I doubt we have different understanding on the effect of
> reflexive operator. Let's discuss this with an example. Say we have two
> relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
> (e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
> 
> If we upgrade (r1;r2) to  (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
> m2)}, it is r1 plus all identity of all elements used in r1's relations.
> 
> So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
> 
>   e1 ->r1 ->e2 ->r2 e3
> 
> A question mark on r1 means both (e1, e3) and (e2, e3) are included in
> the final definition. The r1 is ignore-able in the definition. The event
> before or behind the ignore-able relation both belong to the definition.
> 
> But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
> become empty, because there is no event element in r1's relations.
> 
> So I think the reflexive-transitive operation on cumul-fence cannot make
> this relation optional. You should first have such link in the code.

In Cat, r1? is better described by (following your own wording) "r1 plus
all identity of all elements (i.e. not necessarily in r1)".

As an example, in the scenario at stake, cumul-fence is empty while both
cumul-fence? and cumul-fence* match the identity relation on all events.

Here is a (relatively old, but still accurate AFAICR) article describing
these and other notions as used in Herd:  (cf. table at the bottom)

  https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/herd.html

Said this, I do think the best way to familiarize with these notions and
check one's understanding is to spend time using the herd tool itself.

  Andrea