Received-SPF: pass (google.com: domain of linux-kernel+bounces-188777-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.80.249 as permitted sender) client-ip=147.75.80.249;
Date: Fri, 24 May 2024 10:14:25 -0400
From: Alan Stern <stern@rowland.harvard.edu>
To: Boqun Feng <boqun.feng@gmail.com>
Cc: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>,
  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: <9256f95a-858b-435f-b40a-a4508a1096c9@rowland.harvard.edu>
References: <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>
 <Zk9dXj-f4rANxPep@Boquns-Mac-mini.home>
 <da5241f5-0ae3-40dd-a2fb-8f5307d31dba@rowland.harvard.edu>
 <ZlAAY-BuXSs9xU0m@Boquns-Mac-mini.home>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <ZlAAY-BuXSs9xU0m@Boquns-Mac-mini.home>

On Thu, May 23, 2024 at 07:50:11PM -0700, Boqun Feng wrote:
> On Thu, May 23, 2024 at 09:38:05PM -0400, Alan Stern wrote:
> > On Thu, May 23, 2024 at 08:14:38AM -0700, Boqun Feng wrote:
> > > 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.
> > 
> > I don't really understand the distinction you're making between 
> > syntactic things and semantic things.  For most instructions there's no 
> 
> Syntax is how the code is written, and semantic is how the code is
> executed (in each execution candidate). So if we write a cmpxchg{mb}(),
> and in execution candiates, it could generates a read{MB} event and a
> write{MB} event (succeed case), or a read{MB} event (fail case), "{MB}"
> here doesn't mean it's a full barrier, it only means the event comes
> from a no suffix API. Here "{MB}" only has syntactic meaning (no
> semantic meaning).

Okay, I get it.  Then you might agree that it probably would be better 
to use a different tag here, because the mb tag is already in use with 
other instructions (like smp_mb()) where it does always mean there's a 
full barrier.

> Not really, RMW events contains all events generated from
> read-modify-write primitives, if there is an R event without a rmw
> relation (i.e there is no corresponding write event), it's a failed RWM
> by definition: it cannot be anything else.

Not true.  An R event without an rmw relation could be a READ_ONCE().  
Or a plain read.  The memory model uses the tag to distinguish these 
cases.

> > that it would work is merely an artifact of herd7's internal actions.  I 
> > think it would be much cleaner if herd7 represented these events in some 
> > other way, particularly if we can tell it how.
> > 
> > After all, herd7 already does generate different sets of events for 
> > successful (both R and W) and failed (only R) RMWs.  It's not such a big 
> > stretch to make the R events it generates different in the two cases.
> > 
> 
> I thought we want to simplify the herd internal processing by avoid
> adding mb events in cmpxchg() cases, in the same spirit, if syntactic
> tagging is already good enough, why do we want to make herd complicate?

Herd7 already is complicated by the fact that it needs to handle 
cmpxchg() instructions in two ways: success and failure.  This 
complication is unavoidable.  Adding one extra layer (different tags for 
the different ways) is an insignificant increase in the complication, 
IMO. And it's a net reduction when you compare it to the amount of 
complication currently in the herd7 code.

Also what about cmpxchg_acquire()?  If it fails, it will generate an R 
event with an acquire tag not in the rmw relation.  There is no way to 
tell such events apart from a normal smp_load_acquire(), and so the .cat 
file would have no way to know that the event should not have acquire 
semantics.  I guess we would have to rename this tag, as well.

Alan