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

Hernan Ponce de Leon
2025-02-25T07:59:22Z

On 2/25/2025 5:24 AM, Akira Yokosawa wrote:
> On Thu, 20 Feb 2025 08:14:02 -0800, Paul E. McKenney wrote:
>> From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
>>
>> 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@gmail.com/

Sorry Akira, I lost track of the thread and forgot to answer.

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

Yes, this is correct.

Hernan

>
> So my suggestion is to add a Co-developed-by tag of Hernan here:
>
> Co-developed-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
>> Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
>> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
>> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
>> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
>> Tested-by: Boqun Feng <boqun.feng@gmail.com>
>
> , and let me add a Tested-by:
>
> Tested-by: Akira Yokosawa <akiyks@gmail.com> # 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(-)