Received-SPF: pass (google.com: domain of linux-kernel+bounces-194232-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Date: Wed, 29 May 2024 10:07:44 -0400
From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
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
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
 representation
Message-ID: <b54575b9-ab29-4bcd-ae7a-6132d1e36195@rowland.harvard.edu>
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>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <7e2963a3-d471-4593-9170-7f59aa1ce038@huaweicloud.com>

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