Received-SPF: pass (google.com: domain of linux-kernel+bounces-194253-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
Message-ID: <8c6174c7-a26c-416e-b9b1-2aff2d43dea1@huaweicloud.com>
Date: Wed, 29 May 2024 16:17:36 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
 representation
To: Alan Stern <stern@rowland.harvard.edu>
Cc: Boqun Feng <boqun.feng@gmail.com>, Andrea Parri <parri.andrea@gmail.com>,
 Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>, will@kernel.org,
 peterz@infradead.org, npiggin@gmail.com, dhowells@redhat.com,
 j.alglave@ucl.ac.uk, luc.maranget@inria.fr, paulmck@kernel.org,
 akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
 linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org
References: <20240524151356.236071-1-parri.andrea@gmail.com>
 <1a3c892c-903e-8fd3-24a6-2454c2a55302@huaweicloud.com>
 <ZlSKYA/Y/daiXzfy@andrea>
 <41bc01fa-ce02-4005-a3c2-abfabe1c6927@huaweicloud.com>
 <ZlYbXZSLPmjTKtaE@boqun-archlinux>
 <7e2963a3-d471-4593-9170-7f59aa1ce038@huaweicloud.com>
 <b54575b9-ab29-4bcd-ae7a-6132d1e36195@rowland.harvard.edu>
From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <b54575b9-ab29-4bcd-ae7a-6132d1e36195@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit


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