Re: [PATCH] tools/memory-model: Document herd7 (internal) representation

[Jonas Oberhauser]

Am 5/27/2024 um 3:37 PM schrieb Alan Stern:
> On Mon, May 27, 2024 at 03:28:00PM +0200, Andrea Parri wrote:
> > > > +    |                smp_store_mb | W[once] ->po F[mb]                        |
> > >
> > > I expect this one to be hard-coded in herd7 source code, but I cannot find
> > > it. Can you give me a pointer?
> >
> > smp_store_mb() is currently mapped to { __store{once}(X,V); __fence{mb}; } in
> > the .def file, so it's semantically equivalent to "WRITE_ONCE(); smp_mb();".
>
> Why don't we use this approach for all the value-returning full-barrier
> RMW operations?  That would immediately solve the issue of the
> special-purpose code in herd7, leaving only the matter of how to
> annotate failed RMW operations.


I experimented with that the other day. My idea was to use a new 
__fence{mb-successful-rmw} which would have

  Mb = Mb | Mb-successful-rmw & (domain((po\(po;po));rmw) | 
range(rmw;(po\(po;po)))

to turn only the ordering effect of fences around cmpxchg off (and the 
existance of these fences around unsuccessful cmpxchg would be the only 
difference to the current representation).

Unfortunately I didn't manage to get my changes to the .def file to 
compile (FWIW I'm on herd 7.56+03).

Maybe someone wiser with herd can figure out how to work the .def file.

Best wishes,
   jonas