Received-SPF: pass (google.com: domain of linux-kernel+bounces-203140-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.199.223 as permitted sender) client-ip=147.75.199.223;
Message-ID: <bbc3bd10-3bf5-4b1a-a275-dd328c42e307@huaweicloud.com>
Date: Wed, 5 Jun 2024 21:58:42 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Subject: Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in
 tools/memory-model
To: Alan Stern <stern@rowland.harvard.edu>
Cc: paulmck@kernel.org, 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
References: <20240604152922.495908-1-jonas.oberhauser@huaweicloud.com>
 <88c1ebc8-4805-4d1d-868a-889043899979@rowland.harvard.edu>
From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <88c1ebc8-4805-4d1d-868a-889043899979@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit


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.