Re: [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model

[Akira Yokosawa]

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