Re: Question about PB rule of LKMM

[Kenneth-Lee-2012]

On Mon, Mar 11, 2024 at 11:41:27AM +0800, Kenneth-Lee-2012@xxxxxxxxxxx wrote:
> Date: Mon, 11 Mar 2024 11:41:27 +0800
> From: Kenneth-Lee-2012@xxxxxxxxxxx
> To: Andrea Parri <parri.andrea@xxxxxxxxx>
> Cc: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>, linux-kernel@xxxxxxxxxxxxxxx,
>  paulmck@xxxxxxxxxx
> Subject: Re: Question about PB rule of LKMM
> 
> On Sun, Mar 10, 2024 at 03:27:10AM +0100, Andrea Parri wrote:
> > Date: Sun, 10 Mar 2024 03:27:10 +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
> > 
> > > > 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.
> > 
> 
> Excuse me, May I ask one last question? I tried the herd tool on the
> discussed example. But it seems it is not protected by the hb acyclic
> rule. I can replace the linux-kernel.cat with lock.cat on the test:
> 
> 	P0(int *x)
> 	{
> 		int r1;
> 		WRITE_ONCE(*x, 1);
> 		r1 = READ_ONCE(*x);
> 	}
> 	P1(int *x)
> 	{
> 		WRITE_ONCE(*x, 8);
> 	}
> 	locations[0:r1; x]
> 	exists (0:r1=8)
> 
> It can still ensure the P0:Wx execute before P0:Rx:
> 
> 	Test test Allowed
> 	States 3
> 	0:r1=1; [x]=1;
> 	0:r1=1; [x]=8;
> 	0:r1=8; [x]=8;
> 	Ok
> 	Witnesses
> 	Positive: 1 Negative: 2
> 	Condition exists (0:r1=8)
> 	Observation test Sometimes 1 2
> 
> The example doesn't prove the hb rule is necessary. Is this
> understanding correct? Thanks.

Sorry for disturb, please ignore this. I think the context just to
explain what is prop, not mean to say it can ensure the order.

> 
> >   Andrea
> 
> -- 
> 			-Kenneth Lee