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

[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.

Alan