Received-SPF: pass (google.com: domain of linux-kernel+bounces-188255-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:4601:e00::3 as permitted sender) client-ip=2604:1380:4601:e00::3;
Date: Fri, 24 May 2024 05:30:22 +0200
From: Andrea Parri <parri.andrea@gmail.com>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
	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: <ZlAJzioZnQqNLivU@andrea>
References: <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>
 <Zk4jQe7Vq3N2Vip0@andrea>
 <73e08b17-cb2a-4e14-a94f-7144c5738684@huaweicloud.com>
 <Zk9waJNBwifS/Ops@andrea>
 <1b1485f8-9c84-4221-b955-622dbf2fd953@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <1b1485f8-9c84-4221-b955-622dbf2fd953@huaweicloud.com>

> Do you mean the one example in Table 3?
> What about cmpxchg() or cmpxchg_acquire()?

Yes, Table 3.

The cmpxchg*() primitives were not discussed in the paper.  IIRC, their
representation has not changed since at least 1c27b644c0fd.


> We're definitely getting rid of some lines in herd7, that have been added
> solely for dealing with this specific case of LKMM.

Good.  If the herd7 maintainers are "tired" of dealing with those lines,
that's definitely a big fat "why" to put in a changelog.


> Deal with what, no longer having to learn OCaml to be sure that the LKMM's
> formal definition matches the description in memory_barriers.txt?

Nope.  ;-)   Dealing with the review, testing, and maintainance of a new
representation.


> - it makes it easier to maintain the LKMM in the future, because you don't
> have to work around hidden transformations inside herd7
> - it makes implicit behavior explicit
> - it makes it easier to understand that the formalization matches the
> intention
> - it makes it easier to learn the LKMM from the formalization without having
> to cross-reference every bit with the informal documentation to avoid
> misunderstandings

Jonas -  You write "less hidden", "less implicit", but I keep reading "a
representation I/some people would expect".  We've already acknowledged
that's no deciding factor to abandon the current seasoned representation.

  Andrea