[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <ba7120a5-9208-4506-bf99-2bfa165180c5@rowland.harvard.edu>
Date: Wed, 22 May 2024 14:20:42 -0400
From: Alan Stern <stern@...land.harvard.edu>
To: Andrea Parri <parri.andrea@...il.com>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
Hernan Ponce de Leon <hernan.poncedeleon@...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 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
Powered by blists - more mailing lists