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 (comprising patches 4 and 5) 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.


Have fun,
  jonas


Changes from v1 to v2:
   - addressed several spelling/style issues pointed out by Alan
   - simplified the definition of Marked accesses based on a
      suggestion by Alan

Changes from v2 to v3:
  - addressed imprecise comment pointed out by Boqun
  - addressed the backwards compatibility issue pointed out by Akira
    with help of Hernan: improved version compatibility by adding
    an error message on older versions of herd and relying on a new
    flag -lkmmv1 to select the version
  - integrated recent patches, like the herd representation table
    and primitives like atomic_add_unless or atomic_and_not

Changes from v3 to v4:
  - removed a litmus test (submitted to Paul's larger test repo instead)
  - fixed several formatting/naming issues pointed out by Akira
  - updated the reference herd version number in memory-model/README.md.
    *Note*: this may need to be retouched after herd is updated.
    I also did not update the table under klitmus7 compatibility, which
    I took to refer only to klitmus7, although its header is "herdtools7"



Jonas Oberhauser (5):
  tools/memory-model: Legitimize current use of tags in LKMM macros
  tools/memory-model: Define applicable tags on operation in tools/...
  tools/memory-model: Define effect of Mb tags on RMWs in tools/...
  tools/memory-model: Switch to softcoded herd7 tags
  tools/memory-model: Distinguish between syntactic and semantic tags

 .../Documentation/herd-representation.txt     |  27 +--
 tools/memory-model/README                     |   2 +-
 tools/memory-model/linux-kernel.bell          |  33 ++-
 tools/memory-model/linux-kernel.cat           |  10 +
 tools/memory-model/linux-kernel.cfg           |   1 +
 tools/memory-model/linux-kernel.def           | 196 +++++++++---------
 6 files changed, 150 insertions(+), 119 deletions(-)

-- 
2.34.1

On Mon, Sep 30, 2024 at 12:57:05PM +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 (comprising patches 4 and 5) 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.

Thank you, Jonas!

Queued for further review and testing.  This does need at least an ack to
proceed to mainline (hint to LKMM maintainers).

							Thanx, Paul

> Have fun,
>   jonas
> 
> 
> Changes from v1 to v2:
>    - addressed several spelling/style issues pointed out by Alan
>    - simplified the definition of Marked accesses based on a
>       suggestion by Alan
> 
> Changes from v2 to v3:
>   - addressed imprecise comment pointed out by Boqun
>   - addressed the backwards compatibility issue pointed out by Akira
>     with help of Hernan: improved version compatibility by adding
>     an error message on older versions of herd and relying on a new
>     flag -lkmmv1 to select the version
>   - integrated recent patches, like the herd representation table
>     and primitives like atomic_add_unless or atomic_and_not
> 
> Changes from v3 to v4:
>   - removed a litmus test (submitted to Paul's larger test repo instead)
>   - fixed several formatting/naming issues pointed out by Akira
>   - updated the reference herd version number in memory-model/README.md.
>     *Note*: this may need to be retouched after herd is updated.
>     I also did not update the table under klitmus7 compatibility, which
>     I took to refer only to klitmus7, although its header is "herdtools7"
> 
> 
> 
> Jonas Oberhauser (5):
>   tools/memory-model: Legitimize current use of tags in LKMM macros
>   tools/memory-model: Define applicable tags on operation in tools/...
>   tools/memory-model: Define effect of Mb tags on RMWs in tools/...
>   tools/memory-model: Switch to softcoded herd7 tags
>   tools/memory-model: Distinguish between syntactic and semantic tags
> 
>  .../Documentation/herd-representation.txt     |  27 +--
>  tools/memory-model/README                     |   2 +-
>  tools/memory-model/linux-kernel.bell          |  33 ++-
>  tools/memory-model/linux-kernel.cat           |  10 +
>  tools/memory-model/linux-kernel.cfg           |   1 +
>  tools/memory-model/linux-kernel.def           | 196 +++++++++---------
>  6 files changed, 150 insertions(+), 119 deletions(-)
> 
> -- 
> 2.34.1
>

Hi Paul and Luc,

On Mon, 28 Oct 2024 13:16:23 -0700, Paul E. McKenney wrote:
> On Mon, Sep 30, 2024 at 12:57:05PM +0200, Jonas Oberhauser wrote:
[...]
>> This second step (comprising patches 4 and 5) 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.
> 
> Thank you, Jonas!
> 
> Queued for further review and testing.  This does need at least an ack to
> proceed to mainline (hint to LKMM maintainers).

Paul's lkmm.2024.11.09a branch carries these 7 commits:

  1  tools/memory-model: Add atomic_and()/or()/xor() and add_negative
  2  tools/memory-model: Add atomic_andnot() with its variants
  3  tools/memory-model: Legitimize current use of tags in LKMM macros
  4  tools/memory-model: Define applicable tags on operation in tools/...
  5  tools/memory-model: Define effect of Mb tags on RMWs in tools/...
  6  tools/memory-model: Switch to softcoded herd7 tags
  7  tools/memory-model: Distinguish between syntactic and semantic tags

As the first commit is already incompatible with released versions of herd7,
Paul will have nothing to upstream for v6.13 unless we see a new release of
herdtoolds7 whose herd7 has those atomic RMW bitwise ops and lkmmv2 variant
support in time for the upcoming merge window.

Luc, I have no idea of herdtools7's release procedure, but is there any
chance for us to see such a release of herdtools7, preferably by the end of
November?

        Thanks, Akira