[RFC,memory-model,0/6] LKMM updates
mbox series

Message ID 20190109210706.GA27268@linux.ibm.com
Headers show
Series
  • LKMM updates
Related show

Message

Paul E. McKenney Jan. 9, 2019, 9:07 p.m. UTC
Hello!

This series contains updates for the Linux-kernel memory model:

1-3.	Add SRCU support, courtesy of Alan Stern.

4.	Update README for adding of SRCU support.

5.	Update memory-barriers.txt on enforcing heavy ordering for
	port-I/O accesses, courtesy of Will Deacon.  This one needs
	an ack, preferably by someone from Intel.  Matthew Wilcox
	posted some feedback from an Intel manual here, which might
	be considered to be a close substitute, but...  ;-)

	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org

6.	Update Documentation/explanation.txt to include SRCU support,
	courtesy of Alan Stern.

7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
	Luc Maranget.  This needs an ack.

							Thanx, Paul

------------------------------------------------------------------------

 Documentation/memory-barriers.txt                |    6 
 tools/memory-model/Documentation/explanation.txt |  289 ++++++++++++-----------
 tools/memory-model/README                        |   25 +
 tools/memory-model/linux-kernel.bell             |   37 ++
 tools/memory-model/linux-kernel.cat              |   55 ++--
 tools/memory-model/linux-kernel.def              |    7 
 6 files changed, 250 insertions(+), 169 deletions(-)

Comments

Andrea Parri Jan. 9, 2019, 11:18 p.m. UTC | #1
On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> Hello!
> 
> This series contains updates for the Linux-kernel memory model:
> 
> 1-3.	Add SRCU support, courtesy of Alan Stern.
> 
> 4.	Update README for adding of SRCU support.
> 
> 5.	Update memory-barriers.txt on enforcing heavy ordering for
> 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> 	an ack, preferably by someone from Intel.  Matthew Wilcox
> 	posted some feedback from an Intel manual here, which might
> 	be considered to be a close substitute, but...  ;-)
> 
> 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> 
> 6.	Update Documentation/explanation.txt to include SRCU support,
> 	courtesy of Alan Stern.
> 
> 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> 	Luc Maranget.  This needs an ack.

It seems that

  1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
  
from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
considered that, IIRC, you introduced the primitive and RCU is currently
its only user.)

  Andrea


> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
>  Documentation/memory-barriers.txt                |    6 
>  tools/memory-model/Documentation/explanation.txt |  289 ++++++++++++-----------
>  tools/memory-model/README                        |   25 +
>  tools/memory-model/linux-kernel.bell             |   37 ++
>  tools/memory-model/linux-kernel.cat              |   55 ++--
>  tools/memory-model/linux-kernel.def              |    7 
>  6 files changed, 250 insertions(+), 169 deletions(-)
>
Paul E. McKenney Jan. 9, 2019, 11:40 p.m. UTC | #2
On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > Hello!
> > 
> > This series contains updates for the Linux-kernel memory model:
> > 
> > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > 
> > 4.	Update README for adding of SRCU support.
> > 
> > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > 	posted some feedback from an Intel manual here, which might
> > 	be considered to be a close substitute, but...  ;-)
> > 
> > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > 
> > 6.	Update Documentation/explanation.txt to include SRCU support,
> > 	courtesy of Alan Stern.
> > 
> > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > 	Luc Maranget.  This needs an ack.
> 
> It seems that
> 
>   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
>   
> from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> considered that, IIRC, you introduced the primitive and RCU is currently
> its only user.)

That commit is in -tip:

4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")

So it has already left my -rcu tree.  ;-)

							Thanx, Paul
Andrea Parri Jan. 10, 2019, 12:39 a.m. UTC | #3
On Wed, Jan 09, 2019 at 03:40:43PM -0800, Paul E. McKenney wrote:
> On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> > On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > > Hello!
> > > 
> > > This series contains updates for the Linux-kernel memory model:
> > > 
> > > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > > 
> > > 4.	Update README for adding of SRCU support.
> > > 
> > > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > > 	posted some feedback from an Intel manual here, which might
> > > 	be considered to be a close substitute, but...  ;-)
> > > 
> > > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > > 
> > > 6.	Update Documentation/explanation.txt to include SRCU support,
> > > 	courtesy of Alan Stern.
> > > 
> > > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > > 	Luc Maranget.  This needs an ack.
> > 
> > It seems that
> > 
> >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> >   
> > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > considered that, IIRC, you introduced the primitive and RCU is currently
> > its only user.)
> 
> That commit is in -tip:
> 
> 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> 
> So it has already left my -rcu tree.  ;-)

Oh, you're right: now I see the commit (e.g., with "git show"), but I
don't see the corresponding changes applied to the tree.

  https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
  https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core

Is this expected?

  Andrea


> 
> 							Thanx, Paul
>
Paul E. McKenney Jan. 10, 2019, 4:20 a.m. UTC | #4
On Thu, Jan 10, 2019 at 01:39:52AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 03:40:43PM -0800, Paul E. McKenney wrote:
> > On Thu, Jan 10, 2019 at 12:18:53AM +0100, Andrea Parri wrote:
> > > On Wed, Jan 09, 2019 at 01:07:06PM -0800, Paul E. McKenney wrote:
> > > > Hello!
> > > > 
> > > > This series contains updates for the Linux-kernel memory model:
> > > > 
> > > > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > > > 
> > > > 4.	Update README for adding of SRCU support.
> > > > 
> > > > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > > > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > > > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > > > 	posted some feedback from an Intel manual here, which might
> > > > 	be considered to be a close substitute, but...  ;-)
> > > > 
> > > > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > > > 
> > > > 6.	Update Documentation/explanation.txt to include SRCU support,
> > > > 	courtesy of Alan Stern.
> > > > 
> > > > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > > > 	Luc Maranget.  This needs an ack.
> > > 
> > > It seems that
> > > 
> > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > >   
> > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > its only user.)
> > 
> > That commit is in -tip:
> > 
> > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > 
> > So it has already left my -rcu tree.  ;-)
> 
> Oh, you're right: now I see the commit (e.g., with "git show"), but I
> don't see the corresponding changes applied to the tree.
> 
>   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
>   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> 
> Is this expected?

Are you asking why it is in -tip but not in mainline?  I am not sure,
but given that the merge window was over the holiday season and that
the length of the merge window proved to be shorter than many people
expected it to be, I am not too surprised.  ;-)

							Thanx, Paul
Andrea Parri Jan. 10, 2019, 8:40 a.m. UTC | #5
> > > > It seems that
> > > > 
> > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > >   
> > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > its only user.)
> > > 
> > > That commit is in -tip:
> > > 
> > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > 
> > > So it has already left my -rcu tree.  ;-)
> > 
> > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > don't see the corresponding changes applied to the tree.
> > 
> >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > 
> > Is this expected?
> 
> Are you asking why it is in -tip but not in mainline?  I am not sure,
> but given that the merge window was over the holiday season and that
> the length of the merge window proved to be shorter than many people
> expected it to be, I am not too surprised.  ;-)

Mmh, let me try again:

  $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
  $ cd tip
  $ git checkout -b locking/core origin/locking/core

  $ git show 4607abbcf464
  commit 4607abbcf464ea2be14da444215d05c73025cf6e
  Author: Andrea Parri <andrea.parri@amarulasolutions.com>
  Date:   Mon Dec 3 15:04:49 2018 -0800

      tools/memory-model: Model smp_mb__after_unlock_lock()

  $ cd tools/memory-model
  $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
  File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)

  [aka, linux-kernel.def in tip:locking/core does not have the
   smp_mb__after_unlock_lock() added by 4607abbcf464]

  Andrea


> 
> 							Thanx, Paul
>
Paul E. McKenney Jan. 10, 2019, 2:31 p.m. UTC | #6
On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > It seems that
> > > > > 
> > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > >   
> > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > its only user.)
> > > > 
> > > > That commit is in -tip:
> > > > 
> > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > 
> > > > So it has already left my -rcu tree.  ;-)
> > > 
> > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > don't see the corresponding changes applied to the tree.
> > > 
> > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > 
> > > Is this expected?
> > 
> > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > but given that the merge window was over the holiday season and that
> > the length of the merge window proved to be shorter than many people
> > expected it to be, I am not too surprised.  ;-)
> 
> Mmh, let me try again:
> 
>   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
>   $ cd tip
>   $ git checkout -b locking/core origin/locking/core
> 
>   $ git show 4607abbcf464
>   commit 4607abbcf464ea2be14da444215d05c73025cf6e
>   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
>   Date:   Mon Dec 3 15:04:49 2018 -0800
> 
>       tools/memory-model: Model smp_mb__after_unlock_lock()
> 
>   $ cd tools/memory-model
>   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
>   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> 
>   [aka, linux-kernel.def in tip:locking/core does not have the
>    smp_mb__after_unlock_lock() added by 4607abbcf464]

Color me confused:

------------------------------------------------------------------------

$ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
$ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }

------------------------------------------------------------------------

In addition, it handles this litmus test just fine:

------------------------------------------------------------------------

C MP+polocks

(*
 * Result: Never
 *
 * This litmus test demonstrates how lock acquisitions and releases can
 * stand in for smp_load_acquire() and smp_store_release(), respectively.
 * In other words, when holding a given lock (or indeed after releasing a
 * given lock), a CPU is not only guaranteed to see the accesses that other
 * CPUs made while previously holding that lock, it is also guaranteed
 * to see all prior accesses by those other CPUs.
 *)

{}

P0(int *x, int *y, spinlock_t *mylock)
{
	WRITE_ONCE(*x, 1);
	spin_lock(mylock);
	smp_mb__after_unlock_lock();
	WRITE_ONCE(*y, 1);
	spin_unlock(mylock);
}

P1(int *x, int *y, spinlock_t *mylock)
{
	int r0;
	int r1;

	spin_lock(mylock);
	r0 = READ_ONCE(*y);
	spin_unlock(mylock);
	r1 = READ_ONCE(*x);
}

exists (1:r0=1 /\ 1:r1=0)

------------------------------------------------------------------------

Again, color me confused.

							Thanx, Paul
Alan Stern Jan. 10, 2019, 3:41 p.m. UTC | #7
On Thu, 10 Jan 2019, Paul E. McKenney wrote:

> On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > It seems that
> > > > > > 
> > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > >   
> > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > its only user.)
> > > > > 
> > > > > That commit is in -tip:
> > > > > 
> > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > 
> > > > > So it has already left my -rcu tree.  ;-)
> > > > 
> > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > don't see the corresponding changes applied to the tree.
> > > > 
> > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > 
> > > > Is this expected?
> > > 
> > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > but given that the merge window was over the holiday season and that
> > > the length of the merge window proved to be shorter than many people
> > > expected it to be, I am not too surprised.  ;-)
> > 
> > Mmh, let me try again:
> > 
> >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> >   $ cd tip
> >   $ git checkout -b locking/core origin/locking/core
> > 
> >   $ git show 4607abbcf464
> >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > 
> >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > 
> >   $ cd tools/memory-model
> >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > 
> >   [aka, linux-kernel.def in tip:locking/core does not have the
> >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> 
> Color me confused:
> 
> ------------------------------------------------------------------------
> 
> $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> 
> ------------------------------------------------------------------------
> 
> In addition, it handles this litmus test just fine:
> 
> ------------------------------------------------------------------------
> 
> C MP+polocks
> 
> (*
>  * Result: Never
>  *
>  * This litmus test demonstrates how lock acquisitions and releases can
>  * stand in for smp_load_acquire() and smp_store_release(), respectively.
>  * In other words, when holding a given lock (or indeed after releasing a
>  * given lock), a CPU is not only guaranteed to see the accesses that other
>  * CPUs made while previously holding that lock, it is also guaranteed
>  * to see all prior accesses by those other CPUs.
>  *)
> 
> {}
> 
> P0(int *x, int *y, spinlock_t *mylock)
> {
> 	WRITE_ONCE(*x, 1);
> 	spin_lock(mylock);
> 	smp_mb__after_unlock_lock();
> 	WRITE_ONCE(*y, 1);
> 	spin_unlock(mylock);
> }
> 
> P1(int *x, int *y, spinlock_t *mylock)
> {
> 	int r0;
> 	int r1;
> 
> 	spin_lock(mylock);
> 	r0 = READ_ONCE(*y);
> 	spin_unlock(mylock);
> 	r1 = READ_ONCE(*x);
> }
> 
> exists (1:r0=1 /\ 1:r1=0)
> 
> ------------------------------------------------------------------------
> 
> Again, color me confused.

Andrea's point is that while the 1b52d0186177 commit is present in the
tip repository, it isn't in the locking/core branch.

Alan
Alan Stern Jan. 10, 2019, 3:47 p.m. UTC | #8
On Wed, 9 Jan 2019, Paul E. McKenney wrote:

> Hello!
> 
> This series contains updates for the Linux-kernel memory model:
> 
> 1-3.	Add SRCU support, courtesy of Alan Stern.
> 
> 4.	Update README for adding of SRCU support.
> 
> 5.	Update memory-barriers.txt on enforcing heavy ordering for
> 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> 	an ack, preferably by someone from Intel.  Matthew Wilcox
> 	posted some feedback from an Intel manual here, which might
> 	be considered to be a close substitute, but...  ;-)
> 
> 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> 
> 6.	Update Documentation/explanation.txt to include SRCU support,
> 	courtesy of Alan Stern.
> 
> 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> 	Luc Maranget.  This needs an ack.

Does this one still need an ack?  If so, you may apply mine.

Alan
Paul E. McKenney Jan. 10, 2019, 4:31 p.m. UTC | #9
On Thu, Jan 10, 2019 at 10:41:23AM -0500, Alan Stern wrote:
> On Thu, 10 Jan 2019, Paul E. McKenney wrote:
> 
> > On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > > It seems that
> > > > > > > 
> > > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > >   
> > > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > > its only user.)
> > > > > > 
> > > > > > That commit is in -tip:
> > > > > > 
> > > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > 
> > > > > > So it has already left my -rcu tree.  ;-)
> > > > > 
> > > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > > don't see the corresponding changes applied to the tree.
> > > > > 
> > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > > 
> > > > > Is this expected?
> > > > 
> > > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > > but given that the merge window was over the holiday season and that
> > > > the length of the merge window proved to be shorter than many people
> > > > expected it to be, I am not too surprised.  ;-)
> > > 
> > > Mmh, let me try again:
> > > 
> > >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> > >   $ cd tip
> > >   $ git checkout -b locking/core origin/locking/core
> > > 
> > >   $ git show 4607abbcf464
> > >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> > >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> > >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > > 
> > >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > > 
> > >   $ cd tools/memory-model
> > >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> > >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > > 
> > >   [aka, linux-kernel.def in tip:locking/core does not have the
> > >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> > 
> > Color me confused:
> > 
> > ------------------------------------------------------------------------
> > 
> > $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> > Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> > HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> > $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> > smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> > 
> > ------------------------------------------------------------------------
> > 
> > In addition, it handles this litmus test just fine:
> > 
> > ------------------------------------------------------------------------
> > 
> > C MP+polocks
> > 
> > (*
> >  * Result: Never
> >  *
> >  * This litmus test demonstrates how lock acquisitions and releases can
> >  * stand in for smp_load_acquire() and smp_store_release(), respectively.
> >  * In other words, when holding a given lock (or indeed after releasing a
> >  * given lock), a CPU is not only guaranteed to see the accesses that other
> >  * CPUs made while previously holding that lock, it is also guaranteed
> >  * to see all prior accesses by those other CPUs.
> >  *)
> > 
> > {}
> > 
> > P0(int *x, int *y, spinlock_t *mylock)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	spin_lock(mylock);
> > 	smp_mb__after_unlock_lock();
> > 	WRITE_ONCE(*y, 1);
> > 	spin_unlock(mylock);
> > }
> > 
> > P1(int *x, int *y, spinlock_t *mylock)
> > {
> > 	int r0;
> > 	int r1;
> > 
> > 	spin_lock(mylock);
> > 	r0 = READ_ONCE(*y);
> > 	spin_unlock(mylock);
> > 	r1 = READ_ONCE(*x);
> > }
> > 
> > exists (1:r0=1 /\ 1:r1=0)
> > 
> > ------------------------------------------------------------------------
> > 
> > Again, color me confused.
> 
> Andrea's point is that while the 1b52d0186177 commit is present in the
> tip repository, it isn't in the locking/core branch.

That commit is still in tip/master, so it has not been lost or
forgotten.  ;-)

							Thanx, Paul
Paul E. McKenney Jan. 10, 2019, 7:03 p.m. UTC | #10
On Thu, Jan 10, 2019 at 10:47:26AM -0500, Alan Stern wrote:
> On Wed, 9 Jan 2019, Paul E. McKenney wrote:
> 
> > Hello!
> > 
> > This series contains updates for the Linux-kernel memory model:
> > 
> > 1-3.	Add SRCU support, courtesy of Alan Stern.
> > 
> > 4.	Update README for adding of SRCU support.
> > 
> > 5.	Update memory-barriers.txt on enforcing heavy ordering for
> > 	port-I/O accesses, courtesy of Will Deacon.  This one needs
> > 	an ack, preferably by someone from Intel.  Matthew Wilcox
> > 	posted some feedback from an Intel manual here, which might
> > 	be considered to be a close substitute, but...  ;-)
> > 
> > 	http://lkml.kernel.org/r/20181127192234.GF10377@bombadil.infradead.org
> > 
> > 6.	Update Documentation/explanation.txt to include SRCU support,
> > 	courtesy of Alan Stern.
> > 
> > 7.	Dynamically check SRCU lock-to-unlock matching, courtesy of
> > 	Luc Maranget.  This needs an ack.
> 
> Does this one still need an ack?  If so, you may apply mine.

Applied, thank you!

							Thanx, Paul
Andrea Parri Jan. 10, 2019, 10:46 p.m. UTC | #11
On Thu, Jan 10, 2019 at 08:31:26AM -0800, Paul E. McKenney wrote:
> On Thu, Jan 10, 2019 at 10:41:23AM -0500, Alan Stern wrote:
> > On Thu, 10 Jan 2019, Paul E. McKenney wrote:
> > 
> > > On Thu, Jan 10, 2019 at 09:40:24AM +0100, Andrea Parri wrote:
> > > > > > > > It seems that
> > > > > > > > 
> > > > > > > >   1b52d0186177 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > > >   
> > > > > > > > from linux-rcu/dev got lost; this also needs an ack (probably yours! ;D,
> > > > > > > > considered that, IIRC, you introduced the primitive and RCU is currently
> > > > > > > > its only user.)
> > > > > > > 
> > > > > > > That commit is in -tip:
> > > > > > > 
> > > > > > > 4607abbcf464 ("tools/memory-model: Model smp_mb__after_unlock_lock()")
> > > > > > > 
> > > > > > > So it has already left my -rcu tree.  ;-)
> > > > > > 
> > > > > > Oh, you're right: now I see the commit (e.g., with "git show"), but I
> > > > > > don't see the corresponding changes applied to the tree.
> > > > > > 
> > > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/commit/?h=locking/core&id=4607abbcf464ea2be14da444215d05c73025cf6e
> > > > > >   https://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git/tree/tools/memory-model/linux-kernel.bell?h=locking/core
> > > > > > 
> > > > > > Is this expected?
> > > > > 
> > > > > Are you asking why it is in -tip but not in mainline?  I am not sure,
> > > > > but given that the merge window was over the holiday season and that
> > > > > the length of the merge window proved to be shorter than many people
> > > > > expected it to be, I am not too surprised.  ;-)
> > > > 
> > > > Mmh, let me try again:
> > > > 
> > > >   $ git clone git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip.git
> > > >   $ cd tip
> > > >   $ git checkout -b locking/core origin/locking/core
> > > > 
> > > >   $ git show 4607abbcf464
> > > >   commit 4607abbcf464ea2be14da444215d05c73025cf6e
> > > >   Author: Andrea Parri <andrea.parri@amarulasolutions.com>
> > > >   Date:   Mon Dec 3 15:04:49 2018 -0800
> > > > 
> > > >       tools/memory-model: Model smp_mb__after_unlock_lock()
> > > > 
> > > >   $ cd tools/memory-model
> > > >   $ herd7 -conf linux-kernel.cfg after-unlock-lock-same-cpu.litmus
> > > >   File "after-unlock-lock-same-cpu.litmus": Unknown macro smp_mb__after_unlock_lock (User error)
> > > > 
> > > >   [aka, linux-kernel.def in tip:locking/core does not have the
> > > >    smp_mb__after_unlock_lock() added by 4607abbcf464]
> > > 
> > > Color me confused:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > $ git checkout 4607abbcf464Checking out files: 100% (18397/18397), done.
> > > Previous HEAD position was 4e284b1bf15a rcu: Remove wrapper definitions for obsolete RCU update functions
> > > HEAD is now at 4607abbcf464 tools/memory-model: Model smp_mb__after_unlock_lock()
> > > $ grep smp_mb__after_unlock_lock tools/memory-model/linux-kernel.def 
> > > smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > In addition, it handles this litmus test just fine:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > C MP+polocks
> > > 
> > > (*
> > >  * Result: Never
> > >  *
> > >  * This litmus test demonstrates how lock acquisitions and releases can
> > >  * stand in for smp_load_acquire() and smp_store_release(), respectively.
> > >  * In other words, when holding a given lock (or indeed after releasing a
> > >  * given lock), a CPU is not only guaranteed to see the accesses that other
> > >  * CPUs made while previously holding that lock, it is also guaranteed
> > >  * to see all prior accesses by those other CPUs.
> > >  *)
> > > 
> > > {}
> > > 
> > > P0(int *x, int *y, spinlock_t *mylock)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	spin_lock(mylock);
> > > 	smp_mb__after_unlock_lock();
> > > 	WRITE_ONCE(*y, 1);
> > > 	spin_unlock(mylock);
> > > }
> > > 
> > > P1(int *x, int *y, spinlock_t *mylock)
> > > {
> > > 	int r0;
> > > 	int r1;
> > > 
> > > 	spin_lock(mylock);
> > > 	r0 = READ_ONCE(*y);
> > > 	spin_unlock(mylock);
> > > 	r1 = READ_ONCE(*x);
> > > }
> > > 
> > > exists (1:r0=1 /\ 1:r1=0)
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > Again, color me confused.
> > 
> > Andrea's point is that while the 1b52d0186177 commit is present in the
> > tip repository, it isn't in the locking/core branch.
> 
> That commit is still in tip/master, so it has not been lost or
> forgotten.  ;-)

Sounds reassuring!  ;-)

So, up to today, I've been using tip:locking/core as a reference for our
"almost/tentative-upstream" LKMM changes; well, your reply suggests that
I should have known better... thank you for the patience,

  Andrea


> 
> 							Thanx, Paul
>