Received-SPF: pass (google.com: domain of linux-kernel+bounces-208475-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.80.249 as permitted sender) client-ip=147.75.80.249;
Date: Mon, 10 Jun 2024 08:21:38 -0700
From: "Paul E. McKenney" <paulmck@kernel.org>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: Alan Stern <stern@rowland.harvard.edu>, parri.andrea@gmail.com,
	will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com,
	npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
	luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com,
	joel@joelfernandes.org, urezki@gmail.com, quic_neeraju@quicinc.com,
	frederic@kernel.org, linux-kernel@vger.kernel.org
Subject: Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in
 tools/memory-model
Message-ID: <3c46dba3-575a-4b4d-9ec8-bc06e96a9e40@paulmck-laptop>
Reply-To: paulmck@kernel.org
References: <20240604152922.495908-1-jonas.oberhauser@huaweicloud.com>
 <88c1ebc8-4805-4d1d-868a-889043899979@rowland.harvard.edu>
 <bbc3bd10-3bf5-4b1a-a275-dd328c42e307@huaweicloud.com>
 <cbced924-3f22-484d-8e65-4eebe7c9329a@paulmck-laptop>
 <1aed7106-cb94-451e-93d1-53062e6f3639@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <1aed7106-cb94-451e-93d1-53062e6f3639@huaweicloud.com>

On Mon, Jun 10, 2024 at 10:04:26AM +0200, Jonas Oberhauser wrote:
> 
> 
> Am 6/6/2024 um 6:37 PM schrieb Paul E. McKenney:
> > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
> > > 
> > > 
> > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> > > > On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote:
> > > > > Currently, the effect of several tag on operations is defined only in
> > > > > the herd7 tool's OCaml code as syntax transformations, while the effect
> > > > > of all other tags is defined in tools/memory-model.
> > > > > This asymmetry means that two seemingly analogous definitions in
> > > > > tools/memory-model behave quite differently because the generated
> > > > > representation is sometimes modified by hardcoded behavior in herd7.
> > > > > 
> > > > > It also makes it hard to see that the behavior of the formalization
> > > > > matches the intuition described in explanation.txt without delving into
> > > > > the implementation of herd7.
> > > > > 
> > > > > Furthermore, this hardcoded behavior is hard to maintain inside herd7 and
> > > > > other tools implementing WMM, and has caused several bugs and confusions
> > > > > with the tool maintainers, e.g.:
> > > > > 
> > > > >     https://github.com/MPI-SWS/genmc/issues/22
> > > > >     https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904
> > > > >     https://github.com/hernanponcedeleon/Dat3M/issues/254
> > > > > 
> > > > > It also means that potential future extensions of LKMM with new tags may
> > > > > not work without changing internals of the herd7 tool.
> > > > > 
> > > > > In this patch series, we first emulate the effect of herd7 transformations
> > > > > in tools/memory-model through explicit rules in .cat and .bell files that
> > > > > reference the transformed tags.
> > > > > These transformations do not have any immediate effect with the current
> > > > > herd7 implementation, because they apply after the syntax transformations
> > > > > have already modified those tags.
> > > > > 
> > > > > In a second step, we then distinguish between syntactic tags (that are
> > > > > placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the
> > > > > read and write of an xchg_acquire() operation) and sets of events (that
> > > > > would be defined after the (emulated) transformations, e.g., an Acquire
> > > > > set that includes only on the read of the xchg_acquire(), but "has been
> > > > > removed" from the write).
> > > > > 
> > > > > This second step is incompatible with the current herd7 implementation,
> > > > > since herd7 uses hardcoded tag names to decide what to do with LKMM;
> > > > > therefore, the newly introduced syntactic tags will be ignored or
> > > > > processed incorrectly by herd7.
> > > > 
> > > > The patches look good to me.
> > > > 
> > > > Just to clarify: Your first step encompasses patches 1 - 3, and the
> > > > second step is patch 4.  The first three patches can be applied now, but
> > > > the last one needs to wait until herd7 has been updated.  Is this all
> > > > correct?
> > > 
> > > Exactly.
> > 
> > Just to make sure that I am following along properly...  My belief is
> > that there will be a new version of this series.  Please let me know if
> > I am missing something.
> 
> At least one :))

;-) ;-) ;-)

I will await a later version, then.

								Thanx, Paul