Am 5/29/2024 um 4:07 PM schrieb Alan Stern:
On Wed, May 29, 2024 at 02:37:30PM +0200, Jonas Oberhauser wrote:
Am 5/28/2024 um 7:58 PM schrieb Boqun Feng:
This may not be trivial. Note that cmpxchg() is an expression (it has a
value), so in .def, we want to define it as an expression. However, the
C-like multiple-statement expression is not supported by herd parser, in
other words we want:
{
__fence{mb-successful-rmw};
int tmp = __cmpxchg{once}(...);
__fence{mb-successful-rmw};
tmp;
}
Oh, you're right. Then probably the rule I was violating is that
value-returning macros can not be defined with {} at all.
Given herd's other syntactic limitations, perhaps the best way would be to
introduce these macros as
x = cmpxchg(...) {
__fence{mb-successful-rmw};
x = __cmpxchg{once}(...);
__fence{mb-successful-rmw};
}
since I think x = M(...) is the only way we are allowed to use these macros
anyways.
If we did this, how would the .cat file know to ignore the fence events
when the cmpxchg() fails? It doesn't look like there's anything to
connect the two of them.
Adding the MB tag to the cmpxchg itself seems like the only way forward.
Alan
Something along these lines:
Mb = Mb | Mb-successful-rmw & (domain((po\(po;po));rmw) |
range(rmw;(po\(po;po)))
i.e., using the fact that these mb-successful-rmw fences must appear
directly next to a possibly failing rmw, and looking for successful rmw
directly around them.
I suppose we have to distinguish between the before- and after- fences
though to make it work for cases like
xchg_release();
cmpxchg(); // fails
__xchg_release(...); // is an rmw
__fence{mb-successful-rmw}; // wrong takes mb semantics
x = __cmpxchg{once}(...); // fails
__fence{mb-successful-rmw};
So that would leave us with
x = cmpxchg(...) {
__fence{mb-before-successful-rmw};
x = __cmpxchg{once}(...);
__fence{mb-after-successful-rmw};
}
and in .cat/.bell:
Mb = Mb | Mb-before-successful-rmw & domain((po\(po;po));rmw) |
Mb-after-successful-rmw & range(rmw;(po\(po;po)))
Best wishes,
jonas
