From: Andrea Parri <andrea.parri@amarulasolutions.com>
To: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
mingo@kernel.org, stern@rowland.harvard.edu,
parri.andrea@gmail.com, will.deacon@arm.com,
peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
willy@infradead.org
Subject: Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching
Date: Fri, 11 Jan 2019 00:20:45 +0100 [thread overview]
Message-ID: <20190110232045.GA3908@andrea> (raw)
In-Reply-To: <20190110144049.GK1215@linux.ibm.com>
> > I'm not all that exited about spreading version requirements in the
> > source: we report this requirement in our README, and apparently we
> > already struggle to keep this information up-to-date. So what about
> > squashing something like the below (assume that 7.52 will be released
> > by the time this patch hit mainline; if this won't be the case, we
> > may consider using the development version 7.51+6)? notice that this
> > also removes an (obsolete, at this point) comment from lock.cat.
>
> Sounds like a very good point to me!
>
> Should have pointers in the various files to the README file? Or maybe
> get people used to using scripting that checks versions? Or maybe
> after answering questions for some time, people will get used to
> checking versions?
As discussed off-list: I have no strong opinion on this regard, well,
except that I think we ought to fix the README, somehow (consider my
diff below as a first proposal). Akira actually preceded me on this
and suggested another solution [1].
Andrea
[1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com
>
> Thanx, Paul
>
> > Andrea
> >
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index 9d7d4f23503fd..b362a41358fa1 100644
> > --- a/tools/memory-model/README
> > +++ b/tools/memory-model/README
> > @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
> > REQUIREMENTS
> > ============
> >
> > -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
> > -separately:
> > +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> > +downloaded separately:
> >
> > https://github.com/herd/herdtools7
> >
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index 95bf45f1215fc..8dcb37835b613 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -1,7 +1,5 @@
> > // SPDX-License-Identifier: GPL-2.0+
> > (*
> > - * Requires herd version 7.51+6 or higher.
> > - *
> > * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> > * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > index 305ded17e7411..a059d1a6d8a29 100644
> > --- a/tools/memory-model/lock.cat
> > +++ b/tools/memory-model/lock.cat
> > @@ -6,9 +6,6 @@
> >
> > (*
> > * Generate coherence orders and handle lock operations
> > - *
> > - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
> > - * spin_is_locked() is functional from herd7 version 7.49.
> > *)
> >
> > include "cross.cat"
> >
> >
> >
> > > + *
> > > * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
> > > * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > > * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > > index 1d6a120cde14..0c3f0ef486f4 100644
> > > --- a/tools/memory-model/linux-kernel.def
> > > +++ b/tools/memory-model/linux-kernel.def
> > > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
> > >
> > > // SRCU
> > > srcu_read_lock(X) __srcu{srcu-lock}(X)
> > > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> > > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
> > > synchronize_srcu(X) { __srcu{sync-srcu}(X); }
> > >
> > > // Atomic
> > > --
> > > 2.17.1
> > >
> >
>
next prev parent reply other threads:[~2019-01-10 23:20 UTC|newest]
Thread overview: 28+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-01-09 21:07 [PATCH RFC memory-model 0/6] LKMM updates Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 1/7] tools/memory-model: Rename some RCU relations Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 2/7] tools/memory-model: Refactor " Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 3/7] tools/memory-model: Add SRCU support Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 4/7] tools/memory-model: Update README for addition of SRCU Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 5/7] docs/memory-barriers.txt: Enforce heavy ordering for port I/O accesses Paul E. McKenney
2019-01-11 9:53 ` Peter Zijlstra
2019-02-11 15:30 ` Will Deacon
2019-02-11 17:11 ` Arnd Bergmann
2019-02-11 17:32 ` Will Deacon
2019-01-09 21:07 ` [PATCH RFC LKMM 6/7] tools/memory-model: Update Documentation/explanation.txt to include SRCU support Paul E. McKenney
2019-01-09 21:07 ` [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching Paul E. McKenney
2019-01-10 9:41 ` Andrea Parri
2019-01-10 14:40 ` Paul E. McKenney
2019-01-10 23:20 ` Andrea Parri [this message]
2019-01-11 21:44 ` Paul E. McKenney
2019-01-11 21:57 ` Alan Stern
2019-01-09 23:18 ` [PATCH RFC memory-model 0/6] LKMM updates Andrea Parri
2019-01-09 23:40 ` Paul E. McKenney
2019-01-10 0:39 ` Andrea Parri
2019-01-10 4:20 ` Paul E. McKenney
2019-01-10 8:40 ` Andrea Parri
2019-01-10 14:31 ` Paul E. McKenney
2019-01-10 15:41 ` Alan Stern
2019-01-10 16:31 ` Paul E. McKenney
2019-01-10 22:46 ` Andrea Parri
2019-01-10 15:47 ` Alan Stern
2019-01-10 19:03 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190110232045.GA3908@andrea \
--to=andrea.parri@amarulasolutions.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=j.alglave@ucl.ac.uk \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@linux.ibm.com \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will.deacon@arm.com \
--cc=willy@infradead.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).