Re: LKMM: Making RMW barriers explicit

[Jonas Oberhauser]

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

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

There are probably two ways to achieve this:
a) change herd7 to remove the special behavior for Mb, after that we 
should be able to do everything else in the .cat/.bell/.def files.
b) sidestep herd7's behavior by renaming Mb to _Mb in the .def file,
 and then defining Mb=_Mb in the .bell file, and define the semantics 
of the Mb tag in the .cat files.


The latter would not include modification to herd7, but it's a bit hacky.

I'm not sure if the second way really works since I don't know exactly 
how the herd7 tool does the transpilation,  e.g., if it really looks for 
an Mb tag or rather for the names of the instructions.

Does it make sense?

jonas