[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <8c6174c7-a26c-416e-b9b1-2aff2d43dea1@huaweicloud.com>
Date: Wed, 29 May 2024 16:17:36 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Boqun Feng <boqun.feng@...il.com>, Andrea Parri <parri.andrea@...il.com>,
Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>, will@...nel.org,
peterz@...radead.org, npiggin@...il.com, dhowells@...hat.com,
j.alglave@....ac.uk, luc.maranget@...ia.fr, paulmck@...nel.org,
akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
representation
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
Powered by blists - more mailing lists