Received-SPF: pass (google.com: domain of linux-kernel+bounces-187701-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45d1:ec00::1 as permitted sender) client-ip=2604:1380:45d1:ec00::1;
Feedback-ID: iad51458e:Fastmail
Date: Thu, 23 May 2024 08:14:38 -0700
From: Boqun Feng <boqun.feng@gmail.com>
To: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
	Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@meta.com, parri.andrea@gmail.com, j.alglave@ucl.ac.uk,
	luc.maranget@inria.fr, Joel Fernandes <joel@joelfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit
Message-ID: <Zk9dXj-f4rANxPep@Boquns-Mac-mini.home>
References: <e030f7a4-97e7-4e91-bbae-230ee5c97763@huaweicloud.com>
 <a9bf972c-b5ee-f1c2-36bf-30ba62f419d7@huaweicloud.com>
 <2f20e7cf-7c67-4ad3-8a0c-3c1d01257ae4@rowland.harvard.edu>
 <0c309dd3-f8c1-4945-b8f1-154b2a775216@huaweicloud.com>
 <4286e5b2-5954-4c77-a815-c1c2735d9509@rowland.harvard.edu>
 <58042cf3-e515-4e5f-ab48-1d0d6123c9e9@huaweicloud.com>
 <6174fd09-b287-49ae-b117-c3a36ef3800a@rowland.harvard.edu>
 <7bd31eca-3cf3-4377-a747-ec224262bd2e@huaweicloud.com>
 <35b3fd07-fa85-4244-b9cb-50ea54d9de6a@rowland.harvard.edu>
 <a25f9654-e681-1bad-47ae-ddc519610504@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <a25f9654-e681-1bad-47ae-ddc519610504@huaweicloud.com>

On Thu, May 23, 2024 at 04:26:23PM +0200, Hernan Ponce de Leon wrote:
> On 5/23/2024 4:05 PM, Alan Stern wrote:
> > On Thu, May 23, 2024 at 02:54:05PM +0200, Jonas Oberhauser wrote:
> > > 
> > > 
> > > Am 5/22/2024 um 4:20 PM schrieb Alan Stern:
> > > > It would be better if there was a way to tell herd7 not to add the 'mb
> > > > tag to failed instructions in the first place.  This approach is
> > > > brittle; see below.
> > > 
> > > Hernan told me that in fact that is actually currently the case in herd7.
> > > Failing RMW get assigned the Once tag implicitly.
> > > Another thing that I'd suggest to change.
> > 
> > Indeed.
> > 
> > > > An alternative would be to have a way for the .cat file to remove the
> > > > 'mb tag from a failed RMW instruction.  But I don't know if this is
> > > > feasible.
> > > 
> > > For Mb it's feasible, as there is no Mb read or Mb store.
> > > 
> > > Mb = Mb & (~M | dom(rmw) | range(rmw))
> > > 
> > > However one would want to do the same for Acq and Rel.
> > > 
> > > For that one would need to distinguish e.g. between a read that comes from a
> > > failed rmw instruction, and where the tag would disappear, or a normal
> > > standalone read.
> > > 
> > > For example, by using two different acquire tags, 'acquire and 'rmw-acquire,
> > > and defining
> > > 
> > > Acquire = Acquire | Rmw-acquire & (dom(rmw) | range(rmw))
> > > 
> > > Anyways we can do this change independently. So for now, we don't need
> > > RMW_MB.
> > 
> > Overall, it seems better to have herd7 assign the right tag, but change
> > the way the .def file works so that it can tell herd7 which tag to use
> > in each of the success and failure cases.
> 
> I am not fully sure how herd7 uses the .def file, but I guess something like
> adding a second memory tag to __cmpxchg could work
> 
> cmpxchg(X,V,W) __cmpxchg{mb, once}(X,V,W)
> cmpxchg_relaxed(X,V,W) __cmpxchg{once, once}(X,V,W)
> cmpxchg_acquire(X,V,W) __cmpxchg{acquire, acquire}(X,V,W)
> cmpxchg_release(X,V,W) __cmpxchg{release, release}(X,V,W)
> 

Note that cmpxchg_acquire() and cmpxchg_release() don't have _acqurie
or _release ordering if they fails.

Besides, I'm not sure this is a good idea. Because the "{mb}, {once},
etc" part is a syntax thing, you write a cmpxchg(), it should be
translated to a cmpxchg event with MB tag on. As to failed cmpxchg()
doesn't provide ordering, it's a semantics thing, as Jonas showed that
it can be represent in cat file. As long as it's a semanitc thing and we
can represent in cat file, I don't think we want herd to give a special
treatment.

What you and Jonas looks fine to me, since it moves the semantic bits
from herd internal to cat file.

Regards,
Boqun

> Hernan
> 
> > 
> > > > 	[M] ; po ; [RMW_MB]
> > > > 
> > > > 	[RMW_MB] ; po ; [M]
> > > > 
> > > > This is because events tagged with RMW_MB always are memory accesses,
> > > > and accesses that aren't part of the RMW are already covered by the
> > > > fencerel(Mb) thing above.
> > > 
> > > This has exactly the issue mentioned above - it will cause the rmw to have
> > > an internal strong fence that on powerpc probably isn't there.
> > 
> > Oops, that's right.  Silly oversight on my part.  But at least you
> > understood what I meant.
> > 
> > > We could do (with the assumption that Mb applies only to successful rmw):
> > > 
> > >   	[M] ; po ; [Mb & R]
> > >   	[Mb & W] ; po ; [M]
> > 
> > That works.
> > 
> > Alan
>