Re: LKMM: Making RMW barriers explicit

[Alan Stern]

On Tue, May 21, 2024 at 11:57:29AM +0200, Jonas Oberhauser wrote:
> 
> 
> Am 5/18/2024 um 2:31 AM schrieb Alan Stern:
> > On Thu, May 16, 2024 at 10:44:05AM +0200, Hernan Ponce de Leon wrote:
> > > On 5/16/2024 10:31 AM, Jonas Oberhauser wrote:
> > > > 
> > > > 
> > > > Am 5/16/2024 um 3:43 AM schrieb Alan Stern:
> > > > > Hernan and Jonas:
> > > > > 
> > > > > Can you explain more fully the changes you want to make to herd7 and/or
> > > > > the LKMM?  The goal is to make the memory barriers currently implicit in
> > > > > RMW operations explicit, but I couldn't understand how you propose to do
> > > > > this.
> > > > > 
> > > > > Are you going to change herd7 somehow, and if so, how?  It seems like
> > > > > you should want to provide sufficient information so that the .bell
> > > > > and .cat files can implement the appropriate memory barriers associated
> > > > > with each RMW operation.  What additional information is needed?  And
> > > > > how (explained in English, not by quoting source code) will the .bell
> > > > > and .cat files make use of this information?
> > > > > 
> > > > > Alan
> > > > 
> > > > 
> > > > I don't know whether herd7 needs to be changed. Probably, herd7 does the
> > > > following:
> > > > - if a tag called Mb appears on an rmw instruction (by instruction I
> > > > mean things like xchg(), atomic_inc_return_relaxed()), replace it with
> > > > one of those things:
> > > >     * full mb ; once (the rmw) ; full mb, if a value returning
> > > > (successful) rmw
> > > >     * once (the rmw)   otherwise
> > > > - everything else gets translated 1:1 into some internal representation
> > > 
> > > This is my understanding from reading the source code of CSem.ml in herd7's
> > > repo.
> > > 
> > > Also, this is exactly what dartagnan is currently doing.
> > > 
> > > > 
> > > > What I'm proposing is:
> > > > 1. remove this transpilation step,
> > > > 2. and instead allow the Mb tag to actually appear on RMW instructions
> > > > 3. change the cat file to explicitly define the behavior of the Mb tag
> > > > on RMW instructions
> > > 
> > > These are the exact 3 things I changed in dartagnan for testing what Jonas
> > > proposed.
> > > 
> > > I am not sure if further changes are needed for herd7.

What about failed RMW instructions?  IIRC, herd7 generates just an R for 
these, not both R and W, but won't it still be annotated with an mb tag? 
And wasn't this matter of failed RMWs one of the issues that the two of 
you specifically wanted to make explicit in the memory model, rather 
than implicit in the operation of herd7?

And wasn't another one of these issues the difference between 
value-returning and non-value-returning RMWs?  As far as I can, nothing 
in the .def file specifically mentions this.  There's the noreturn tag 
in the .bell file, but nothing in the .def file says which instructions 
it applies to.  Or are we supposed to know that it automatically applies 
to all __atomic_op() instances?

> > Okay, good.  This answers the first part of what I asked.  What about
> > the second part?  That is, how will the changes to the .def, .bell, and
> > .cat files achieve your goals?
> > 
> > Alan
> 
> 
> Firstly, we'd allow 'mb as a barrier mode in events, e.g.

You mean as a mode in RMW events.  'mb already is a mode for F events.

> instructions RMW[{'once,'acquire,'release,'mb}]
> 
> then the Mb tags would appear in the graph. And then I'd define the ordering
> explicitly. One way is to say that an Mb tag orders all memory accesses
> before(or at) the tag with all memory accesses after(or at) the tag, except
> the accesses of the rmw with each other.

I don't think you need to add very much.  The .cat file already defines 
the mb relation as including the term:

	([M] ; fencerel(Mb) ; [M])

All that's needed is to replace the fencerel(Mb) with something more 
general...

> This is the same as the full fence before the read, which orders all memory
> accesses before the read with every access after(or at) the read,
> plus the full fence after the write, which orders all memory accesses
> before(or at) the write with all accesses after the write.
> 
> That would be done by adding
> 
>      [M] ; (po \ rmw) & (po^?; [RMW_MB] ; po^?) ; [M]

.. like this.

> to ppo.

You need to update the definition of mb, not ppo.  And the RMW_MB above 
looks wrong; shouldn't it be just Mb?

Also, is the "\ rmw" part really necessary?  I don't think it makes any 
difference; the memory model already knows that the read part of an RMW 
has to happen before the write part.

> One could also split it into two rules to keep with the "two full fences"
> analogy. Maybe a good way would be like this:
> 
>      [M] ; po; [RMW_MB & R] ; po^? ; [M]
> 
>      [M] ; po^?; [RMW_MB & W] ; po ; [M]

My preference is for the first approach.

Alan