Re: Question about PB rule of LKMM

[Kenneth-Lee-2012]

On Fri, Mar 08, 2024 at 10:38:09PM +0100, Andrea Parri wrote:
> Date: Fri, 8 Mar 2024 22:38:09 +0100
> From: Andrea Parri <parri.andrea@xxxxxxxxx>
> To: Kenneth-Lee-2012@xxxxxxxxxxx
> Cc: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>, linux-kernel@xxxxxxxxxxxxxxx,
>  paulmck@xxxxxxxxxx
> Subject: Re: Question about PB rule of LKMM
> 
> > In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
> > it uses the following example to explain the prop relation:
> > 
> > 	P0()
> > 	{
> > 		int r1;
> > 
> > 		WRITE_ONCE(x, 1);
> > 		r1 = READ_ONCE(x);
> > 	}
> > 
> > 	P1()
> > 	{
> > 		WRITE_ONCE(x, 8);
> > 	}
> > 
> > if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
> > explained with the operational model. But according to the definition of
> > prop,
> > 
> >   let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> > 
> > The link should contain a cumul-fence, which doesn't exist in the
> > example.
> 
> 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.

-Kenneth

>   Andrea