Received-SPF: pass (google.com: domain of linux-kernel+bounces-186525-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45d1:ec00::1 as permitted sender) client-ip=2604:1380:45d1:ec00::1;
Date: Wed, 22 May 2024 18:54:25 +0200
From: Andrea Parri <parri.andrea@gmail.com>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
	Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@meta.com, boqun.feng@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: <Zk4jQe7Vq3N2Vip0@andrea>
References: <72c804c8-2511-4349-a823-bc1de8bb729e@rowland.harvard.edu>
 <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>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <6174fd09-b287-49ae-b117-c3a36ef3800a@rowland.harvard.edu>

Alan, all,

("randomly" picking a recent post in the thread, after having observed
this discussion for a while...)

> 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.

AFAIU, changing the herd representation to generate mb-accesses in place
of certain mb-fences...

> If you do want to use this approach, it should be simplified.  All you 
> need is:
> 
> 	[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.

.. and updating the .cat file to the effects of something like

  -let mb = ([M] ; fencerel(Mb) ; [M]) |
  +let mb = (([M] ; po? ; [Mb] ; po? ; [M]) \ id) |

.. can hardly be called "making RMW barriers explicit".  (So much so
that the first commit in PR #865 was titled "Remove explicit barriers
from RMWs".  :-))

Overall, this discussion rather seems to confirm the close link between
tools/memory-model/ and herdtools7.  (After all, to what extent could
any putative RMW_MB be considered "explicit" without _knowing the under-
lying representation of the RMW operations...)  My understanding is that
this discussion was at least in part motivated by a desire to experiment
and familiarize with the current herd representation (that does indeed
require some getting-used-to...); this suggests, as some of you already
mentioned, to add some comments or a .txt in tools/memory-model/ in order
to document such representation and ameliorate that experience.  OTOH, I
must admit, I'm unable to see here sufficient motivation(tm) for changing
the current representation (and model): not the how, but the why...

  Andrea