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...
> 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". :-))
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...
Andrea
