Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[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?

Alan