Received-SPF: pass (google.com: domain of linux-kernel+bounces-98106-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.199.223 as permitted sender) client-ip=147.75.199.223;
Message-ID: <tencent_6175BDD3A69360BE460116C8CE650E992108@qq.com>
Sender: kenneth-lee-2012@foxmail.com
Date: Sun, 10 Mar 2024 10:52:20 +0800
From: Kenneth-Lee-2012@foxmail.com
To: Andrea Parri <parri.andrea@gmail.com>
Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org,
	paulmck@kernel.org
Subject: Re: Question about PB rule of LKMM
References: <ZejC+lutRuwXQrMz@andrea>
 <Zenip+8BDM3p+MUh@andrea>
 <eb8f2a21-d388-424d-8504-ccd7bdb53a93@rowland.harvard.edu>
 <ZeoFBkB1BeTdEQsn@andrea>
 <bde188b0-1c5b-4b3b-94de-395a52fc37ce@rowland.harvard.edu>
 <ZeoQvj3l6moF9KdQ@andrea>
 <tencent_3FCF3AA5E98BC9395F98803764A6B2F7CC07@qq.com>
 <ZeuFQdk/zcjkILbC@andrea>
 <tencent_454C12FBD6076C20C3955565E6D6354E4F0A@qq.com>
 <Ze0afrfXMe4oJ4ez@andrea>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <Ze0afrfXMe4oJ4ez@andrea>

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@gmail.com>
> To: Kenneth-Lee-2012@foxmail.com
> Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org,
>  paulmck@kernel.org
> 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.
> 

Ah, thank you very much for the link. The information is even not in the
herd7 manual. That's way I following the understanding from some mathematical
text such as: "The reflexive transitive closure of R is denoted R∗, and
is defined as the reflexive closure of the transitive closure of R".
It doesn't rely the total event set (S).

I will spend more time to try the herd itself. Thanks.

-Kenneth

>   Andrea