Message-ID: <1aed7106-cb94-451e-93d1-53062e6f3639@huaweicloud.com>
Date: Mon, 10 Jun 2024 10:04:26 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: paulmck@...nel.org
Cc: Alan Stern <stern@...land.harvard.edu>, parri.andrea@...il.com,
 will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
 npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
 luc.maranget@...ia.fr, akiyks@...il.com, dlustig@...dia.com,
 joel@...lfernandes.org, urezki@...il.com, quic_neeraju@...cinc.com,
 frederic@...nel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in
 tools/memory-model



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 :))

Have fun,
   jonas

Powered by blists - more mailing lists