Am 5/23/2024 um 4:05 PM schrieb Alan Stern:
On Thu, May 23, 2024 at 02:54:05PM +0200, Jonas Oberhauser wrote:
Am 5/22/2024 um 4:20 PM schrieb Alan Stern:
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.
Hernan told me that in fact that is actually currently the case in herd7.
Failing RMW get assigned the Once tag implicitly.
Another thing that I'd suggest to change.
Indeed.
An alternative would be to have a way for the .cat file to remove the
'mb tag from a failed RMW instruction. But I don't know if this is
feasible.
For Mb it's feasible, as there is no Mb read or Mb store.
Mb = Mb & (~M | dom(rmw) | range(rmw))
However one would want to do the same for Acq and Rel.
For that one would need to distinguish e.g. between a read that comes from a
failed rmw instruction, and where the tag would disappear, or a normal
standalone read.
For example, by using two different acquire tags, 'acquire and 'rmw-acquire,
and defining
Acquire = Acquire | Rmw-acquire & (dom(rmw) | range(rmw))
Anyways we can do this change independently. So for now, we don't need
RMW_MB.
Overall, it seems better to have herd7 assign the right tag, but change
the way the .def file works so that it can tell herd7 which tag to use
in each of the success and failure cases.
Yes, that would be good.
In principle herd should already support this kind of logic for e.g. C11
which also has distinct success and failure modes.
But of course I don't know if there's syntax to make this change in
.def, let alone what it would look like.
But at least you
understood what I meant.
I do try :) (: :)
We could do (with the assumption that Mb applies only to successful rmw):
[M] ; po ; [Mb & R]
[Mb & W] ; po ; [M]
That works.
Ok, I'll prepare a patch for this and Andrea or anyone else can still
interject.
I suppose the patch would not change the semantics at all with the
current herd7, since Mb does not appear on any reads and writes for the
time being.
best wishes,
jonas
