Re: LKMM: Making RMW barriers explicit

[Jonas Oberhauser]

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