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
