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: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