Re: [PATCH memory-model 6/7] tools/memory-model: Switch to softcoded herd7 tags
Akira Yokosawa <[email protected]>
| Newsgroups | dev.linux.lists.lkmm,org.kernel.vger.linux-arch,org.kernel.vger.linux-kernel |
|---|---|
| Message-ID | <[email protected]> |
On Thu, 20 Feb 2025 08:14:02 -0800, Paul E. McKenney wrote: > From: Jonas Oberhauser <[email protected]> > > 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/[email protected]/ , 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 <[email protected]> > Signed-off-by: Hernan Ponce de Leon <[email protected]> > Signed-off-by: Jonas Oberhauser <[email protected]> > Signed-off-by: Paul E. McKenney <[email protected]> > Reviewed-by: Boqun Feng <[email protected]> > Tested-by: Boqun Feng <[email protected]> , and let me add a Tested-by: Tested-by: Akira Yokosawa <[email protected]> # 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(-)