Date: Wed, 22 May 2024 21:48:18 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
To: Alan Stern <stern@...land.harvard.edu>,
 Andrea Parri <parri.andrea@...il.com>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
 "Paul E. McKenney" <paulmck@...nel.org>, linux-kernel@...r.kernel.org,
 linux-arch@...r.kernel.org, kernel-team@...a.com, boqun.feng@...il.com,
 j.alglave@....ac.uk, luc.maranget@...ia.fr,
 Joel Fernandes <joel@...lfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit

On 5/22/2024 8:20 PM, Alan Stern wrote:
> 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.

I can give my motivation as a tool developer. It would be much simpler 
if one could find all the information to support lkmm in 
tools/memory-model/ (in the form of the model + some comments or a .txt 
to cover those things we cannot move out of the tool implementation), 
rather than having to dive into herd7 code.

Hernan

> 
> Alan

Powered by blists - more mailing lists