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

[Jonas Oberhauser]

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.