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
