Received-SPF: pass (google.com: domain of linux-kernel+bounces-194261-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.48.161 as permitted sender) client-ip=147.75.48.161;
Date: Wed, 29 May 2024 10:24:26 -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: <2e34674c-2443-4345-8bc7-8c950a47f621@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>
 <b54575b9-ab29-4bcd-ae7a-6132d1e36195@rowland.harvard.edu>
 <8c6174c7-a26c-416e-b9b1-2aff2d43dea1@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <8c6174c7-a26c-416e-b9b1-2aff2d43dea1@huaweicloud.com>

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.

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.

Alan