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.
