Re: [PATCH memory-model 6/7] tools/memory-model: Switch to softcoded herd7 tags

From: Akira Yokosawa
Date: Mon Feb 24 2025 - 23:24:54 EST


On Thu, 20 Feb 2025 08:14:02 -0800, Paul E. McKenney wrote:
> From: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
>
> A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
> behavior of simply ignoring any softcoded tags in the .def and .bell files. We
> port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
> and reporting an error if the LKMM is used without this switch.
>
> To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
> RMW which do not return a value and define atomic_add_unless with an Mb tag in
> linux-kernel.def.
>
> We update the herd-representation.txt accordingly and clarify some of the
> resulting combinations.
>

Having failed to hear from Jonas or Hernan in response to my question at:

https://lore.kernel.org/lkmm/ec97f28e-31ad-4a45-ac87-fab91e27d4ee@xxxxxxxxx/

, let me guess. Past contributions strongly suggest that Hernan looks after
herd7 changes and Jonas takes care of LKMM side of changes.

So my suggestion is to add a Co-developed-by tag of Hernan here:

Co-developed-by: Hernan Ponce de Leon <hernan.poncedeleon@xxxxxxxxxxxxxxx>
> Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@xxxxxxxxxxxxxxx>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
> Reviewed-by: Boqun Feng <boqun.feng@xxxxxxxxx>
> Tested-by: Boqun Feng <boqun.feng@xxxxxxxxx>

, and let me add a Tested-by:

Tested-by: Akira Yokosawa <akiyks@xxxxxxxxx> # herdtools7.7.58

Thanks, Akira

> ---
> .../Documentation/herd-representation.txt | 27 ++++++++++---------
> tools/memory-model/README | 2 +-
> tools/memory-model/linux-kernel.bell | 3 +++
> tools/memory-model/linux-kernel.cfg | 1 +
> tools/memory-model/linux-kernel.def | 18 +++++++------
> 5 files changed, 30 insertions(+), 21 deletions(-)