Received-SPF: pass (google.com: domain of linux-kernel+bounces-186608-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Date: Wed, 22 May 2024 14:20:42 -0400
From: Alan Stern <stern@rowland.harvard.edu>
To: Andrea Parri <parri.andrea@gmail.com>
Cc: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
  Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>,
  "Paul E. McKenney" <paulmck@kernel.org>, linux-kernel@vger.kernel.org,
  linux-arch@vger.kernel.org, kernel-team@meta.com, boqun.feng@gmail.com,
  j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
  Joel Fernandes <joel@joelfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit
Message-ID: <ba7120a5-9208-4506-bf99-2bfa165180c5@rowland.harvard.edu>
References: <72c804c8-2511-4349-a823-bc1de8bb729e@rowland.harvard.edu>
 <e030f7a4-97e7-4e91-bbae-230ee5c97763@huaweicloud.com>
 <a9bf972c-b5ee-f1c2-36bf-30ba62f419d7@huaweicloud.com>
 <2f20e7cf-7c67-4ad3-8a0c-3c1d01257ae4@rowland.harvard.edu>
 <0c309dd3-f8c1-4945-b8f1-154b2a775216@huaweicloud.com>
 <4286e5b2-5954-4c77-a815-c1c2735d9509@rowland.harvard.edu>
 <58042cf3-e515-4e5f-ab48-1d0d6123c9e9@huaweicloud.com>
 <6174fd09-b287-49ae-b117-c3a36ef3800a@rowland.harvard.edu>
 <Zk4jQe7Vq3N2Vip0@andrea>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <Zk4jQe7Vq3N2Vip0@andrea>

On Wed, May 22, 2024 at 06:54:25PM +0200, Andrea Parri wrote:
> Alan, all,
> 
> ("randomly" picking a recent post in the thread, after having observed
> this discussion for a while...)
> 
> > It would be better if there was a way to tell herd7 not to add the 'mb 
> > tag to failed instructions in the first place.  This approach is 
> > brittle; see below.
> 
> AFAIU, changing the herd representation to generate mb-accesses in place
> of certain mb-fences...

I believe herd7 already generates mb accesses (not fences) for certain 
RMW operations.  But then it does some post-processing on them, and that 
post-processing is what we are thinking of changing.

> > If you do want to use this approach, it should be simplified.  All you 
> > need is:
> > 
> > 	[M] ; po ; [RMW_MB]
> > 
> > 	[RMW_MB] ; po ; [M]
> > 
> > This is because events tagged with RMW_MB always are memory accesses, 
> > and accesses that aren't part of the RMW are already covered by the 
> > fencerel(Mb) thing above.
> 
> ... and updating the .cat file to the effects of something like
> 
>   -let mb = ([M] ; fencerel(Mb) ; [M]) |
>   +let mb = (([M] ; po? ; [Mb] ; po? ; [M]) \ id) |
> 
> ... can hardly be called "making RMW barriers explicit".  (So much so
> that the first commit in PR #865 was titled "Remove explicit barriers
> from RMWs".  :-))

There is another point, something we didn't spell out explicitly in the 
email discussion.  Namely, in linux-kernel.def there is a long list of 
instructions along with corresponding herd7 implementation instructions, 
and those instructions explicitly contain either {once}, {acquire}, 
{release}, or {mb} tags.  So to a large extent, these barriers already 
are explicit in the memory model.  Not in the .cat file, but in the .def 
file.

What is not so explicit is how the {mb} tag works.  Its operation isn't 
as simple as the operation of the {acquire} and {release} tags; those 
just modify the R or W access in the RMW pair as you would expect.  
Instead, an {mb} tag says to insert strong memory barriers before the R 
access and after the W access.  This is more or less what the 
post-processing mentioned earlier does, and Jonas and Hernan want to 
move this out of herd7 and into the memory model.

> Overall, this discussion rather seems to confirm the close link between
> tools/memory-model/ and herdtools7.  (After all, to what extent could
> any putative RMW_MB be considered "explicit" without _knowing the under-
> lying representation of the RMW operations...)  My understanding is that
> this discussion was at least in part motivated by a desire to experiment
> and familiarize with the current herd representation (that does indeed
> require some getting-used-to...); this suggests, as some of you already
> mentioned, to add some comments or a .txt in tools/memory-model/ in order
> to document such representation and ameliorate that experience.  OTOH, I
> must admit, I'm unable to see here sufficient motivation(tm) for changing
> the current representation (and model): not the how, but the why...

Well, it's not a big change.  And in my opinion, if something can be 
moved out of herd7's innards and into the memory model files, then doing 
so is generally a good idea.

However, I do agree that there will still be a close link between 
tools/memory-model/ and herdtools7.  This may be unavoidable, at least 
to some extent, but any way to reduce it is worth considering.

Alan