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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date: Wed, 29 May 2024 16:33:21 +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:24 PM schrieb Alan Stern:
> On Wed, May 29, 2024 at 04:17:36PM +0200, Jonas Oberhauser wrote:
>>
>>
>> Am 5/29/2024 um 4:07 PM schrieb Alan Stern:
>>> On Wed, May 29, 2024 at 02:37:30PM +0200, Jonas Oberhauser wrote:
>>>> 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)))
> 
> It's messy.  Associating the fences directly with the RMW event(s) by
> adding the MB tags is much cleaner, IMO.

I agree.

> Also, does the syntax you are proposing require changes to herd7?  I'm
> not aware that it is currently able to parse that kind of definition.

Indeed, herd7 can't deal with this syntax right now.

    jonas