* [GIT PULL tools] Linux kernel memory model
@ 2018-01-25 9:34 Paul E. McKenney
2018-01-29 6:57 ` Ingo Molnar
2018-02-08 18:41 ` Patrick Bellasi
0 siblings, 2 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-01-25 9:34 UTC (permalink / raw)
To: mingo
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks
Hello, Ingo,
This pull request contains a single commit that adds a memory model to
the tools directory. This memory model can (roughly speaking) be thought
of as an automated version of memory-barriers.txt. It is written in the
"cat" language, which is executable by the externally provided "herd7"
simulator, which exhaustively explores the state space of small litmus
tests.
This memory model is accompanied by extensive documentation on its use
and its design. Two versions have been sent to LKML and feedback
incorporated:
1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
This model has been presented and demoed at a number of Linux gatherings,
including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
Plumbers Conference, which featured a workshop helping a number of Linux
kernel hackers install and use the tool.
This memory model has matured to the point where it would be good to include
it in the Linux kernel, for example, to allow it to track changes as new
hardware and use cases are added. We expect the rate of change to be similar
to that of Documentation/memory-barriers.txt.
This memory model is available in the git repository at:
git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
----------------------------------------------------------------
Paul E. McKenney (1):
Automate memory-barriers.txt; provide Linux-kernel memory model
tools/memory-model/Documentation/cheatsheet.txt | 30 +
tools/memory-model/Documentation/explanation.txt | 1840 ++++++++++++++++++++
tools/memory-model/Documentation/recipes.txt | 570 ++++++
tools/memory-model/Documentation/references.txt | 107 ++
tools/memory-model/MAINTAINERS | 15 +
tools/memory-model/README | 220 +++
tools/memory-model/linux-kernel.bell | 53 +
tools/memory-model/linux-kernel.cat | 124 ++
tools/memory-model/linux-kernel.cfg | 21 +
tools/memory-model/linux-kernel.def | 108 ++
.../litmus-tests/CoRR+poonceonce+Once.litmus | 19 +
.../litmus-tests/CoRW+poonceonce+Once.litmus | 18 +
.../litmus-tests/CoWR+poonceonce+Once.litmus | 18 +
.../litmus-tests/CoWW+poonceonce.litmus | 11 +
.../litmus-tests/IRIW+mbonceonces+OnceOnce.litmus | 35 +
.../litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 33 +
.../litmus-tests/ISA2+poonceonces.litmus | 28 +
...cerelease+poacquirerelease+poacquireonce.litmus | 28 +
.../litmus-tests/LB+ctrlonceonce+mbonceonce.litmus | 23 +
.../LB+poacquireonce+pooncerelease.litmus | 21 +
.../litmus-tests/LB+poonceonces.litmus | 21 +
.../litmus-tests/MP+onceassign+derefonce.litmus | 25 +
tools/memory-model/litmus-tests/MP+polocks.litmus | 24 +
.../litmus-tests/MP+poonceonces.litmus | 20 +
.../MP+pooncerelease+poacquireonce.litmus | 20 +
.../memory-model/litmus-tests/MP+porevlocks.litmus | 24 +
.../litmus-tests/MP+wmbonceonce+rmbonceonce.litmus | 22 +
.../memory-model/litmus-tests/R+mbonceonces.litmus | 21 +
.../memory-model/litmus-tests/R+poonceonces.litmus | 19 +
tools/memory-model/litmus-tests/README | 125 ++
.../memory-model/litmus-tests/S+poonceonces.litmus | 19 +
.../S+wmbonceonce+poacquireonce.litmus | 20 +
.../litmus-tests/SB+mbonceonces.litmus | 23 +
.../litmus-tests/SB+poonceonces.litmus | 21 +
.../litmus-tests/WRC+poonceonces+Once.litmus | 27 +
.../WRC+pooncerelease+rmbonceonce+Once.litmus | 28 +
.../Z6.0+pooncelock+poonceLock+pombonce.litmus | 33 +
.../Z6.0+pooncelock+pooncelock+pombonce.litmus | 32 +
...ooncerelease+poacquirerelease+mbonceonce.litmus | 28 +
tools/memory-model/lock.cat | 99 ++
40 files changed, 3973 insertions(+)
create mode 100644 tools/memory-model/Documentation/cheatsheet.txt
create mode 100644 tools/memory-model/Documentation/explanation.txt
create mode 100644 tools/memory-model/Documentation/recipes.txt
create mode 100644 tools/memory-model/Documentation/references.txt
create mode 100644 tools/memory-model/MAINTAINERS
create mode 100644 tools/memory-model/README
create mode 100644 tools/memory-model/linux-kernel.bell
create mode 100644 tools/memory-model/linux-kernel.cat
create mode 100644 tools/memory-model/linux-kernel.cfg
create mode 100644 tools/memory-model/linux-kernel.def
create mode 100644 tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
create mode 100644 tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
create mode 100644 tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
create mode 100644 tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
create mode 100644 tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
create mode 100644 tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
create mode 100644 tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
create mode 100644 tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
create mode 100644 tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
create mode 100644 tools/memory-model/litmus-tests/LB+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+polocks.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+porevlocks.litmus
create mode 100644 tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
create mode 100644 tools/memory-model/litmus-tests/R+mbonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/R+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/README
create mode 100644 tools/memory-model/litmus-tests/S+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
create mode 100644 tools/memory-model/litmus-tests/SB+mbonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/SB+poonceonces.litmus
create mode 100644 tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
create mode 100644 tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
create mode 100644 tools/memory-model/lock.cat
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-25 9:34 [GIT PULL tools] Linux kernel memory model Paul E. McKenney
@ 2018-01-29 6:57 ` Ingo Molnar
2018-01-29 9:54 ` Paul E. McKenney
2018-02-08 18:41 ` Patrick Bellasi
1 sibling, 1 reply; 26+ messages in thread
From: Ingo Molnar @ 2018-01-29 6:57 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra
hi Paul,
* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> Hello, Ingo,
>
> This pull request contains a single commit that adds a memory model to
> the tools directory. This memory model can (roughly speaking) be thought
> of as an automated version of memory-barriers.txt. It is written in the
> "cat" language, which is executable by the externally provided "herd7"
> simulator, which exhaustively explores the state space of small litmus
> tests.
>
> This memory model is accompanied by extensive documentation on its use
> and its design. Two versions have been sent to LKML and feedback
> incorporated:
>
> 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
>
> This model has been presented and demoed at a number of Linux gatherings,
> including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> Plumbers Conference, which featured a workshop helping a number of Linux
> kernel hackers install and use the tool.
>
> This memory model has matured to the point where it would be good to include
> it in the Linux kernel, for example, to allow it to track changes as new
> hardware and use cases are added. We expect the rate of change to be similar
> to that of Documentation/memory-barriers.txt.
>
> This memory model is available in the git repository at:
>
> git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
>
> for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
>
> Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
Looks good to me, but the commit is not in the master branch of your tree, which
branch should I pull?
Thanks,
Ingo
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-29 6:57 ` Ingo Molnar
@ 2018-01-29 9:54 ` Paul E. McKenney
2018-01-31 9:00 ` Ingo Molnar
0 siblings, 1 reply; 26+ messages in thread
From: Paul E. McKenney @ 2018-01-29 9:54 UTC (permalink / raw)
To: Ingo Molnar
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra
On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote:
>
> hi Paul,
>
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
>
> > Hello, Ingo,
> >
> > This pull request contains a single commit that adds a memory model to
> > the tools directory. This memory model can (roughly speaking) be thought
> > of as an automated version of memory-barriers.txt. It is written in the
> > "cat" language, which is executable by the externally provided "herd7"
> > simulator, which exhaustively explores the state space of small litmus
> > tests.
> >
> > This memory model is accompanied by extensive documentation on its use
> > and its design. Two versions have been sent to LKML and feedback
> > incorporated:
> >
> > 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> > 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
> >
> > This model has been presented and demoed at a number of Linux gatherings,
> > including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> > the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> > Plumbers Conference, which featured a workshop helping a number of Linux
> > kernel hackers install and use the tool.
> >
> > This memory model has matured to the point where it would be good to include
> > it in the Linux kernel, for example, to allow it to track changes as new
> > hardware and use cases are added. We expect the rate of change to be similar
> > to that of Documentation/memory-barriers.txt.
> >
> > This memory model is available in the git repository at:
> >
> > git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
> >
> > for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
> >
> > Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
>
> Looks good to me, but the commit is not in the master branch of your tree, which
> branch should I pull?
Oops!!! The branch is lkmm-for-mingo.
Please accept my apologies for the implicit maintainer treasure hunt!
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-29 9:54 ` Paul E. McKenney
@ 2018-01-31 9:00 ` Ingo Molnar
2018-01-31 10:08 ` Peter Zijlstra
` (2 more replies)
0 siblings, 3 replies; 26+ messages in thread
From: Ingo Molnar @ 2018-01-31 9:00 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote:
> >
> > hi Paul,
> >
> > * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> >
> > > Hello, Ingo,
> > >
> > > This pull request contains a single commit that adds a memory model to
> > > the tools directory. This memory model can (roughly speaking) be thought
> > > of as an automated version of memory-barriers.txt. It is written in the
> > > "cat" language, which is executable by the externally provided "herd7"
> > > simulator, which exhaustively explores the state space of small litmus
> > > tests.
> > >
> > > This memory model is accompanied by extensive documentation on its use
> > > and its design. Two versions have been sent to LKML and feedback
> > > incorporated:
> > >
> > > 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> > > 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
> > >
> > > This model has been presented and demoed at a number of Linux gatherings,
> > > including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> > > the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> > > Plumbers Conference, which featured a workshop helping a number of Linux
> > > kernel hackers install and use the tool.
> > >
> > > This memory model has matured to the point where it would be good to include
> > > it in the Linux kernel, for example, to allow it to track changes as new
> > > hardware and use cases are added. We expect the rate of change to be similar
> > > to that of Documentation/memory-barriers.txt.
> > >
> > > This memory model is available in the git repository at:
> > >
> > > git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
> > >
> > > for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
> > >
> > > Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
> >
> > Looks good to me, but the commit is not in the master branch of your tree, which
> > branch should I pull?
>
> Oops!!! The branch is lkmm-for-mingo.
>
> Please accept my apologies for the implicit maintainer treasure hunt!
No problem, was able to pull it!
I really like this formal description of of the Linux kernel memory coherency
model and the extensive documentation around it. Clearly a lot of effort went
into this work!
A couple of questions:
- Would it be possible to include all the nice descriptions of the litmus tests in
the tests themselves? Right now it's a bit weird that most of them come with
zero explanations, but the tools/memory-model/litmus-tests/README lists most of
them.
- Similary, some of the high level descriptions in tools/memory-model/README
should probably propagated into the source code files as well: for example
both tools/memory-model/lock.cat and linux-kernel.cat could be improved that
way.
- Could tools/memory-model/MAINTAINERS be added to the main Linux MAINTAINERS file
as well, like we do for other bits of tooling?
- There's no description about why the .bell file is called 'bell' and what
language/syntax it is in - I had to search around to figure out that it's a
"Bell extension" to .cat files. This aspect IMHO isn't really obvious to first
time readers so a bit more explanation would be nice.
- A high level question: have you considered calling it the "Linux kernel memory
coherency model", instead of the "Linux memory model"? Another naming would be
the "Linux kernel memory access model" as memory-barriers.txt calls it.
The "memory model" name is overly generic, ambiguous and somewhat misleading,
as we usually mean the virtual memory layout/model when we say "memory model".
GCC too uses it in that sense: 'small memory model' and 'large memory model' -
which too is about VM layout, not multiprocessing coherency.
- A long term question: have you considered and would it make sense to generate a
memory-barriers.txt like file directly into Documentation/locking/, using the
formal description? That way any changes/extensions/fixes to the model could be
tracked on a high level, without readers having to understand the formal
representation.
In any case, the base commit is certainly nice and clean and I've pulled it into
tip:locking/core for a v4.17 merge.
I believe these additional improvements (to the extent you agree with doing them!)
could/should be done as add-on commits on top of this existing commit.
Thanks,
Ingo
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-31 9:00 ` Ingo Molnar
@ 2018-01-31 10:08 ` Peter Zijlstra
2018-01-31 23:53 ` Paul E. McKenney
2018-02-01 1:17 ` Paul E. McKenney
2018-02-03 8:48 ` Paul E. McKenney
2 siblings, 1 reply; 26+ messages in thread
From: Peter Zijlstra @ 2018-01-31 10:08 UTC (permalink / raw)
To: Ingo Molnar
Cc: Paul E. McKenney, linux-kernel, linux-arch, stern, parri.andrea,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks, Thomas Gleixner,
Linus Torvalds
On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote:
> - Similary, some of the high level descriptions in tools/memory-model/README
> should probably propagated into the source code files as well: for example
> both tools/memory-model/lock.cat and linux-kernel.cat could be improved that
> way.
This is something both Will and me have on our todo list, sadly we've
not had any time to work on this due to this pesky spectre crap.
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-31 10:08 ` Peter Zijlstra
@ 2018-01-31 23:53 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-01-31 23:53 UTC (permalink / raw)
To: Peter Zijlstra
Cc: Ingo Molnar, linux-kernel, linux-arch, stern, parri.andrea,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks, Thomas Gleixner,
Linus Torvalds
On Wed, Jan 31, 2018 at 11:08:22AM +0100, Peter Zijlstra wrote:
> On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote:
> > - Similary, some of the high level descriptions in tools/memory-model/README
> > should probably propagated into the source code files as well: for example
> > both tools/memory-model/lock.cat and linux-kernel.cat could be improved that
> > way.
>
> This is something both Will and me have on our todo list, sadly we've
> not had any time to work on this due to this pesky spectre crap.
Spectre permitting, this would be very cool!
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-31 9:00 ` Ingo Molnar
2018-01-31 10:08 ` Peter Zijlstra
@ 2018-02-01 1:17 ` Paul E. McKenney
2018-02-01 6:57 ` Ingo Molnar
2018-02-02 4:46 ` Boqun Feng
2018-02-03 8:48 ` Paul E. McKenney
2 siblings, 2 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-01 1:17 UTC (permalink / raw)
To: Ingo Molnar
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote:
>
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
>
> > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote:
> > >
> > > hi Paul,
> > >
> > > * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> > >
> > > > Hello, Ingo,
> > > >
> > > > This pull request contains a single commit that adds a memory model to
> > > > the tools directory. This memory model can (roughly speaking) be thought
> > > > of as an automated version of memory-barriers.txt. It is written in the
> > > > "cat" language, which is executable by the externally provided "herd7"
> > > > simulator, which exhaustively explores the state space of small litmus
> > > > tests.
> > > >
> > > > This memory model is accompanied by extensive documentation on its use
> > > > and its design. Two versions have been sent to LKML and feedback
> > > > incorporated:
> > > >
> > > > 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> > > > 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
> > > >
> > > > This model has been presented and demoed at a number of Linux gatherings,
> > > > including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> > > > the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> > > > Plumbers Conference, which featured a workshop helping a number of Linux
> > > > kernel hackers install and use the tool.
> > > >
> > > > This memory model has matured to the point where it would be good to include
> > > > it in the Linux kernel, for example, to allow it to track changes as new
> > > > hardware and use cases are added. We expect the rate of change to be similar
> > > > to that of Documentation/memory-barriers.txt.
> > > >
> > > > This memory model is available in the git repository at:
> > > >
> > > > git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
> > > >
> > > > for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
> > > >
> > > > Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
> > >
> > > Looks good to me, but the commit is not in the master branch of your tree, which
> > > branch should I pull?
> >
> > Oops!!! The branch is lkmm-for-mingo.
> >
> > Please accept my apologies for the implicit maintainer treasure hunt!
>
> No problem, was able to pull it!
>
> I really like this formal description of of the Linux kernel memory coherency
> model and the extensive documentation around it. Clearly a lot of effort went
> into this work!
Glad you like it, and kudos to my partners in crime! ;-)
> A couple of questions:
>
> - Would it be possible to include all the nice descriptions of the litmus tests in
> the tests themselves? Right now it's a bit weird that most of them come with
> zero explanations, but the tools/memory-model/litmus-tests/README lists most of
> them.
Good point, and should be doable.
> - Similary, some of the high level descriptions in tools/memory-model/README
> should probably propagated into the source code files as well: for example
> both tools/memory-model/lock.cat and linux-kernel.cat could be improved that
> way.
I gratefully accept Peter's and Will's offer here. ;-)
> - Could tools/memory-model/MAINTAINERS be added to the main Linux MAINTAINERS file
> as well, like we do for other bits of tooling?
Easily enough. Should we have both files, or just keep the
information in the main Linux MAINTAINERS file, eliminating
tools/memory-model/MAINTAINERS? I have the usual concerns about
duplicating this information.
> - There's no description about why the .bell file is called 'bell' and what
> language/syntax it is in - I had to search around to figure out that it's a
> "Bell extension" to .cat files. This aspect IMHO isn't really obvious to first
> time readers so a bit more explanation would be nice.
This was named before my time, but I believe that it is a play on "bell
the cat" (https://en.wikipedia.org/wiki/Belling_the_cat).
Anyway, by convention (roughly speaking) the .bell file defines events
(loads, stores, atomic operations, barriers) and the .cat file defines
how those events interact, as in what cycles are permitted and not.
> - A high level question: have you considered calling it the "Linux kernel memory
> coherency model", instead of the "Linux memory model"? Another naming would be
> the "Linux kernel memory access model" as memory-barriers.txt calls it.
> The "memory model" name is overly generic, ambiguous and somewhat misleading,
> as we usually mean the virtual memory layout/model when we say "memory model".
> GCC too uses it in that sense: 'small memory model' and 'large memory model' -
> which too is about VM layout, not multiprocessing coherency.
Interesting point. There is a lot of history calling these things
"memory models", so there may be different tradeoffs for different people.
Wikipedia has these two, which might indicate that the ambiguity is not
too problematic:
https://en.wikipedia.org/wiki/Memory_model_(programming)
https://en.wikipedia.org/wiki/Memory_address#Memory_models
But worth some thought!
> - A long term question: have you considered and would it make sense to generate a
> memory-barriers.txt like file directly into Documentation/locking/, using the
> formal description? That way any changes/extensions/fixes to the model could be
> tracked on a high level, without readers having to understand the formal
> representation.
I hadn't considered this at all, actually. ;-)
The sections of memory-barriers.txt dealing with MMIO ordering would need
to stay hand-generated, but they are a very small fraction of the total.
The herd7 tool is capable of generating cool diagrams sort of like
this one: https://static.lwn.net/images/2017/mm-model/rmo-acyclic.png,
which might replace at least some of the hand-generated ASCII-art
diagrams.
Although I do confess harboring some skepticism about being able to
generated high-quality text, there is no denying that it would be
valuable to be able to do so.
> In any case, the base commit is certainly nice and clean and I've pulled it into
> tip:locking/core for a v4.17 merge.
Very good!
> I believe these additional improvements (to the extent you agree with doing them!)
> could/should be done as add-on commits on top of this existing commit.
Sounds good!
Would you prefer a pull request or a patch series for these?
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-01 1:17 ` Paul E. McKenney
@ 2018-02-01 6:57 ` Ingo Molnar
2018-02-01 23:14 ` Paul E. McKenney
2018-02-02 4:46 ` Boqun Feng
1 sibling, 1 reply; 26+ messages in thread
From: Ingo Molnar @ 2018-02-01 6:57 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> > I believe these additional improvements (to the extent you agree with doing them!)
> > could/should be done as add-on commits on top of this existing commit.
>
> Sounds good!
>
> Would you prefer a pull request or a patch series for these?
Patch series would be nice, for review and later application to the locking tree.
Thanks,
Ingo
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-01 6:57 ` Ingo Molnar
@ 2018-02-01 23:14 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-01 23:14 UTC (permalink / raw)
To: Ingo Molnar
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Thu, Feb 01, 2018 at 07:57:42AM +0100, Ingo Molnar wrote:
>
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
>
> > > I believe these additional improvements (to the extent you agree with doing them!)
> > > could/should be done as add-on commits on top of this existing commit.
> >
> > Sounds good!
> >
> > Would you prefer a pull request or a patch series for these?
>
> Patch series would be nice, for review and later application to the locking tree.
Works for me!
I will curate the series on branch lkmm in my -rcu tree, and send the
series out non-RFC when I believe that it is ready for you.
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-01 1:17 ` Paul E. McKenney
2018-02-01 6:57 ` Ingo Molnar
@ 2018-02-02 4:46 ` Boqun Feng
2018-02-02 5:40 ` Paul E. McKenney
1 sibling, 1 reply; 26+ messages in thread
From: Boqun Feng @ 2018-02-02 4:46 UTC (permalink / raw)
To: Paul E. McKenney
Cc: Ingo Molnar, linux-kernel, linux-arch, stern, parri.andrea,
j.alglave, luc.maranget, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
[-- Attachment #1: Type: text/plain, Size: 1735 bytes --]
On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote:
[...]
> > - A long term question: have you considered and would it make sense to generate a
> > memory-barriers.txt like file directly into Documentation/locking/, using the
> > formal description? That way any changes/extensions/fixes to the model could be
> > tracked on a high level, without readers having to understand the formal
> > representation.
>
> I hadn't considered this at all, actually. ;-)
>
> The sections of memory-barriers.txt dealing with MMIO ordering would need
> to stay hand-generated, but they are a very small fraction of the total.
> The herd7 tool is capable of generating cool diagrams sort of like
> this one: https://static.lwn.net/images/2017/mm-model/rmo-acyclic.png,
> which might replace at least some of the hand-generated ASCII-art
> diagrams.
>
Which reminds me, one thing we could start with is to try to convert all
the examples with litmus tests. Has this been done somewhere (e.g. in
your litmus github repo)? If not, I can try if you think that's a good
idea.
Regards,
Boqun
> Although I do confess harboring some skepticism about being able to
> generated high-quality text, there is no denying that it would be
> valuable to be able to do so.
>
> > In any case, the base commit is certainly nice and clean and I've pulled it into
> > tip:locking/core for a v4.17 merge.
>
> Very good!
>
> > I believe these additional improvements (to the extent you agree with doing them!)
> > could/should be done as add-on commits on top of this existing commit.
>
> Sounds good!
>
> Would you prefer a pull request or a patch series for these?
>
> Thanx, Paul
>
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-02 4:46 ` Boqun Feng
@ 2018-02-02 5:40 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-02 5:40 UTC (permalink / raw)
To: Boqun Feng
Cc: Ingo Molnar, linux-kernel, linux-arch, stern, parri.andrea,
j.alglave, luc.maranget, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Fri, Feb 02, 2018 at 12:46:03PM +0800, Boqun Feng wrote:
> On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote:
> [...]
> > > - A long term question: have you considered and would it make sense to generate a
> > > memory-barriers.txt like file directly into Documentation/locking/, using the
> > > formal description? That way any changes/extensions/fixes to the model could be
> > > tracked on a high level, without readers having to understand the formal
> > > representation.
> >
> > I hadn't considered this at all, actually. ;-)
> >
> > The sections of memory-barriers.txt dealing with MMIO ordering would need
> > to stay hand-generated, but they are a very small fraction of the total.
> > The herd7 tool is capable of generating cool diagrams sort of like
> > this one: https://static.lwn.net/images/2017/mm-model/rmo-acyclic.png,
> > which might replace at least some of the hand-generated ASCII-art
> > diagrams.
>
> Which reminds me, one thing we could start with is to try to convert all
> the examples with litmus tests. Has this been done somewhere (e.g. in
> your litmus github repo)? If not, I can try if you think that's a good
> idea.
That would be very helpful, thank you!
There are probably some that are already in the litmus-tests directory,
but I suspect that most are not yet converted. So please do!
Thanx, Paul
> Regards,
> Boqun
>
> > Although I do confess harboring some skepticism about being able to
> > generated high-quality text, there is no denying that it would be
> > valuable to be able to do so.
> >
> > > In any case, the base commit is certainly nice and clean and I've pulled it into
> > > tip:locking/core for a v4.17 merge.
> >
> > Very good!
> >
> > > I believe these additional improvements (to the extent you agree with doing them!)
> > > could/should be done as add-on commits on top of this existing commit.
> >
> > Sounds good!
> >
> > Would you prefer a pull request or a patch series for these?
> >
> > Thanx, Paul
> >
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-31 9:00 ` Ingo Molnar
2018-01-31 10:08 ` Peter Zijlstra
2018-02-01 1:17 ` Paul E. McKenney
@ 2018-02-03 8:48 ` Paul E. McKenney
2018-02-03 22:10 ` Alan Stern
2 siblings, 1 reply; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-03 8:48 UTC (permalink / raw)
To: Ingo Molnar
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote:
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote:
[ . . . ]
> A couple of questions:
>
> - Would it be possible to include all the nice descriptions of the litmus tests in
> the tests themselves? Right now it's a bit weird that most of them come with
> zero explanations, but the tools/memory-model/litmus-tests/README lists most of
> them.
Please see below for an initial patch to this effect. This activity
proved to be more productive than expected for these tests, which certainly
supports our assertion that locking needs more testing...
MP+polocks.litmus
MP+porevlocks.litmus
These are allowed by the current model, which surprised me a bit,
given that even powerpc would forbid them. Is the rationale
that a lock-savvy compiler could pull accesses into the lock's
critical section and then reorder those accesses? Or does this
constitute a bug in our model of locking?
(And these were allowed when I wrote recipes.txt, embarrassingly
enough...)
Z6.0+pooncelock+poonceLock+pombonce.litmus
This was forbidden when I wrote recipes.txt, but now is allowed.
The header comment for smp_mb__after_spinlock() makes it pretty
clear that it must be forbidden. So this one is a bug in our
model of locking.
I did not add comments to the above three, but please see below for a
patch for the remaining litmus tests.
Thoughts?
Thanx, Paul
------------------------------------------------------------------------
commit af55b248bec4ac2513d5715b10724d379099bb64
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Sat Feb 3 00:04:49 2018 -0800
litmus_tests: Add comments explaining tests' purposes
This commit adds comments to the litmus tests summarizing what these
tests are intended to demonstrate.
Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
index 5b83d57f6ac5..8e8ae8989085 100644
--- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoRR+poonceonce+Once
+(*
+ * Test of read-read coherence, that is, whether or not two successive
+ * reads from the same variable are ordered. They should be ordered,
+ * that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
index fab91c13d52c..0078ecd76f5e 100644
--- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoRW+poonceonce+Once
+(*
+ * Test of read-write coherence, that is, whether or not a read from a
+ * given variable followed by a write to that same variable are ordered.
+ * This should be ordered, that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
index 6a35ec2042ea..c9d342c8fbec 100644
--- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoWR+poonceonce+Once
+(*
+ * Test of write-read coherence, that is, whether or not a write to a
+ * given variable followed by a read from that same variable are ordered.
+ * They should be ordered, that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
index 32a96b832021..ad51c7b17f7b 100644
--- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
+++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
@@ -1,5 +1,11 @@
C CoWW+poonceonce
+(*
+ * Test of write-write coherence, that is, whether or not two successive
+ * writes to the same variable are ordered. They should be ordered, that
+ * is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
index 7eba2c68992b..8a58abce69fe 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
@@ -1,5 +1,14 @@
C IRIW+mbonceonces+OnceOnce
+(*
+ * Test of independent reads from independent writes with smp_mb()
+ * between each pairs of reads. In other words, is smp_mb() sufficient to
+ * cause two different reading processes to agree on the order of a pair
+ * of writes, where each write is to a different variable by a different
+ * process? The smp_mb()s should be sufficient, that is, this test should
+ * be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
index b0556c6c75d4..c736cd372207 100644
--- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
@@ -1,5 +1,14 @@
C IRIW+poonceonces+OnceOnce
+(*
+ * Test of independent reads from independent writes with nothing
+ * between each pairs of reads. In other words, is anything at all
+ * needed to cause two different reading processes to agree on the order
+ * of a pair of writes, where each write is to a different variable by a
+ * different process? Something is needed, in other words, this test
+ * should be allowed.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
index 9a1a233d70c3..1f1c4220c92d 100644
--- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
@@ -1,5 +1,13 @@
C ISA2+poonceonces
+(*
+ * Given a release-acquire chain ordering the first process's store
+ * against the last process's load, is ordering preserved if all of the
+ * smp_store_release() invocations be replaced by WRITE_ONCE() and all
+ * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
+ * The answer is "no", that is, this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
index 235195e87d4e..aa4b25838519 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
@@ -1,5 +1,14 @@
C ISA2+pooncerelease+poacquirerelease+poacquireonce
+(*
+ * This litmus test demonstrates that a release-acquire chain suffices
+ * to order P0()'s initial write against P2()'s final read. The reason
+ * that the release-acquire chain suffices is because in all but one
+ * case (P2() to P0()), each process reads from the preceding process's
+ * write. In memory-model-speak, there is only one non-reads-from
+ * (AKA non-rf) link, so release-acquire is all that is needed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
index dd5ac3a8974a..0b65048ad4db 100644
--- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
@@ -1,5 +1,14 @@
C LB+ctrlonceonce+mbonceonce
+(*
+ * This litmus test demonstrates that lightweight ordering suffices for
+ * the load-buffering pattern, in other words, preventing all processes
+ * reading from the preceding process's write. In this example, the
+ * combination of a control dependency and a full memory barrier are to do
+ * the trick. (But the full memory barrier could be replaced with another
+ * control dependency and order would still be maintained.)
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
index 47bd61319d93..1d1f45ff1940 100644
--- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
+++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
@@ -1,5 +1,12 @@
C LB+poacquireonce+pooncerelease
+(*
+ * Does a release-acquire pair suffice for the load-buffering litmus
+ * test, where each process reads from one of two variables then writes
+ * to the other? The answer is "yes", that is, this test should be
+ * forbidden.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
index a5cdf027e34b..383e3e0adb4e 100644
--- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
@@ -1,5 +1,11 @@
C LB+poonceonces
+(*
+ * Can the counter-intuitive outcome for the load-buffering pattern
+ * be prevented even with no explicit ordering? The answer should be
+ * "no", that is, this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 1a2fe5830381..86ddc88a26a2 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -1,5 +1,12 @@
C MP+onceassign+derefonce.litmus
+(*
+ * This litmus test demonstrates that rcu_assign_pointer() and
+ * rcu_dereference() suffice to ensure that an RCU reader will not see
+ * pre-initialization garbage when it traverses an RCU-protected data
+ * structure containing a newly inserted element.
+ *)
+
{
y=z;
z=0;
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 46e1ac7ba126..16a1d45e3fde 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -1,5 +1,11 @@
C MP+poonceonces
+(*
+ * Can the counter-intuitive message-passing outcome be prevented with
+ * no ordering at all? The answer should be "no", that is, this test
+ * should be prohibited.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index 0b00cc7293ba..f7fbe2636287 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -1,5 +1,11 @@
C MP+pooncerelease+poacquireonce
+(*
+ * This litmus test demonstrates that smp_store_release() and
+ * smp_load_acquire() provide sufficient ordering for the message-passing
+ * pattern.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
index 604ad41ea0c2..3d53ba138acd 100644
--- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
@@ -1,5 +1,11 @@
C MP+wmbonceonce+rmbonceonce
+(*
+ * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
+ * sufficient ordering for the message-passing pattern. However, it
+ * is usually better to use smp_store_release() and smp_load_acquire().
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
index e69b9e3e9436..4d64e547f1cd 100644
--- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
@@ -1,5 +1,12 @@
C R+mbonceonces
+(*
+ * This is the fully ordered (via smp_mb()) version of one of the classic
+ * counterintuitive litmus tests that illustrates the effects of store
+ * propagation delays. This test should be forbidden, but weaking either
+ * of the barriers would cause the resulting test to be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
index f7a12e00f82d..e75295b4e7c1 100644
--- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
@@ -1,5 +1,11 @@
C R+poonceonces
+(*
+ * This is the unordered (via smp_mb()) version of one of the classic
+ * counterintuitive litmus tests that illustrates the effects of store
+ * propagation delays. This test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
index d0d541c8ec7d..7fe16920a228 100644
--- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
@@ -1,5 +1,13 @@
C S+poonceonces
+(*
+ * Starting with a two-process release-acquire chain ordering P0()'s
+ * first store against P1()'s final load, if the smp_store_release()
+ * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
+ * READ_ONCE(), is ordering preserved. The answer is "of course not!",
+ * so this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
index 1d292d0d6603..f78ce120863b 100644
--- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
@@ -1,5 +1,11 @@
C S+wmbonceonce+poacquireonce
+(*
+ * Can a smp_wmb(), instead of a release, and an acquire order a prior
+ * store against a subsequent store? The answer should be "yes", so
+ * this test should be forbidden.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
index b76caa5af1af..476542cd4a49 100644
--- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
@@ -1,5 +1,12 @@
C SB+mbonceonces
+(*
+ * This litmus test demonstrates that full memory barriers suffice to
+ * order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process read. (Locking and RCU can also
+ * suffice, but not much else.)
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
index c1797e03807e..40d519408ea6 100644
--- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
@@ -1,5 +1,11 @@
C SB+poonceonces
+(*
+ * This litmus test demonstrates that at least some ordering is required
+ * to order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process read. This test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
index f5e7c92f61cc..0780a67cf3bd 100644
--- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -1,5 +1,11 @@
C WRC+poonceonces+Once
+(*
+ * This litmus test is an extension of the message-passing pattern, where
+ * the first write is moved to a separate process. But because this test
+ * has no ordering at all, it should be allowed.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
index e3d0018025dd..070166d435e5 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
@@ -1,5 +1,11 @@
C WRC+pooncerelease+rmbonceonce+Once
+(*
+ * This litmus test is an extension of the message-passing pattern, where
+ * the first write is moved to a separate process. Because it features
+ * a release and a read memory barrier, it should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
index c9a1f1a49ae1..8c723892716f 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
@@ -1,5 +1,11 @@
C Z6.0+pooncelock+pooncelock+pombonce
+(*
+ * This example demonstrates that a pair of accesses made by different
+ * processes each while holding a given lock will not necessarily be
+ * seen as ordered by a third process not holding that lock.
+ *)
+
{}
P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
index 25409a033514..8b0b1b3ca348 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
@@ -1,5 +1,17 @@
C Z6.0+pooncerelease+poacquirerelease+mbonceonce
+(*
+ * This litmus test shows that a release-acquire chain, while sufficient
+ * when there is but one non-reads-from (AKA non-rf) link, does not suffice
+ * if there is more than one. Of the three processes, only P1() reads from
+ * P0's write, which means that there are two non-rf links: P1() to P2()
+ * is a write-to-write link (AKA a "coherence" or just "co" link) and P2()
+ * to P0() is a read-to-write link (AKA a "from-reads" or just "fr" link).
+ * When there are two or more non-rf links, you typically will need one
+ * full barrier for each non-rf link. (Exceptions include some cases
+ * involving locking.)
+ *)
+
{}
P0(int *x, int *y)
^ permalink raw reply related [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-03 8:48 ` Paul E. McKenney
@ 2018-02-03 22:10 ` Alan Stern
2018-02-04 9:16 ` Paul E. McKenney
0 siblings, 1 reply; 26+ messages in thread
From: Alan Stern @ 2018-02-03 22:10 UTC (permalink / raw)
To: Paul E. McKenney
Cc: Ingo Molnar, linux-kernel, linux-arch, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sat, 3 Feb 2018, Paul E. McKenney wrote:
> Please see below for an initial patch to this effect. This activity
> proved to be more productive than expected for these tests, which certainly
> supports our assertion that locking needs more testing...
>
> MP+polocks.litmus
> MP+porevlocks.litmus
>
> These are allowed by the current model, which surprised me a bit,
> given that even powerpc would forbid them. Is the rationale
> that a lock-savvy compiler could pull accesses into the lock's
> critical section and then reorder those accesses? Or does this
> constitute a bug in our model of locking?
>
> (And these were allowed when I wrote recipes.txt, embarrassingly
> enough...)
>
> Z6.0+pooncelock+poonceLock+pombonce.litmus
>
> This was forbidden when I wrote recipes.txt, but now is allowed.
> The header comment for smp_mb__after_spinlock() makes it pretty
> clear that it must be forbidden. So this one is a bug in our
> model of locking.
I just tried testing these under the most recent version of herd, and
all three were forbidden.
Alan
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-03 22:10 ` Alan Stern
@ 2018-02-04 9:16 ` Paul E. McKenney
2018-02-04 10:17 ` Paul E. McKenney
0 siblings, 1 reply; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-04 9:16 UTC (permalink / raw)
To: Alan Stern
Cc: Ingo Molnar, linux-kernel, linux-arch, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote:
> On Sat, 3 Feb 2018, Paul E. McKenney wrote:
>
> > Please see below for an initial patch to this effect. This activity
> > proved to be more productive than expected for these tests, which certainly
> > supports our assertion that locking needs more testing...
> >
> > MP+polocks.litmus
> > MP+porevlocks.litmus
> >
> > These are allowed by the current model, which surprised me a bit,
> > given that even powerpc would forbid them. Is the rationale
> > that a lock-savvy compiler could pull accesses into the lock's
> > critical section and then reorder those accesses? Or does this
> > constitute a bug in our model of locking?
> >
> > (And these were allowed when I wrote recipes.txt, embarrassingly
> > enough...)
> >
> > Z6.0+pooncelock+poonceLock+pombonce.litmus
> >
> > This was forbidden when I wrote recipes.txt, but now is allowed.
> > The header comment for smp_mb__after_spinlock() makes it pretty
> > clear that it must be forbidden. So this one is a bug in our
> > model of locking.
>
> I just tried testing these under the most recent version of herd, and
> all three were forbidden.
And they do for me as well once I upgraded to the most recent version of
herd. Whew!!!
Boy, we weren't kidding when we said that you need to us the latest
and greatest herd7, now were we? ;-)
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-04 9:16 ` Paul E. McKenney
@ 2018-02-04 10:17 ` Paul E. McKenney
2018-02-04 16:29 ` Andrea Parri
2018-02-04 16:37 ` Alan Stern
0 siblings, 2 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-04 10:17 UTC (permalink / raw)
To: Alan Stern
Cc: Ingo Molnar, linux-kernel, linux-arch, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sun, Feb 04, 2018 at 01:16:01AM -0800, Paul E. McKenney wrote:
> On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote:
> > On Sat, 3 Feb 2018, Paul E. McKenney wrote:
> >
> > > Please see below for an initial patch to this effect. This activity
> > > proved to be more productive than expected for these tests, which certainly
> > > supports our assertion that locking needs more testing...
> > >
> > > MP+polocks.litmus
> > > MP+porevlocks.litmus
> > >
> > > These are allowed by the current model, which surprised me a bit,
> > > given that even powerpc would forbid them. Is the rationale
> > > that a lock-savvy compiler could pull accesses into the lock's
> > > critical section and then reorder those accesses? Or does this
> > > constitute a bug in our model of locking?
> > >
> > > (And these were allowed when I wrote recipes.txt, embarrassingly
> > > enough...)
> > >
> > > Z6.0+pooncelock+poonceLock+pombonce.litmus
> > >
> > > This was forbidden when I wrote recipes.txt, but now is allowed.
> > > The header comment for smp_mb__after_spinlock() makes it pretty
> > > clear that it must be forbidden. So this one is a bug in our
> > > model of locking.
> >
> > I just tried testing these under the most recent version of herd, and
> > all three were forbidden.
>
> And they do for me as well once I upgraded to the most recent version of
> herd. Whew!!!
>
> Boy, we weren't kidding when we said that you need to us the latest
> and greatest herd7, now were we? ;-)
And here is the updated commit adding comments to the litmus test,
which adds comments for the three litmus tests added above. I have also
marked this commit with "EXP" indicating that it has not yet had time
for review. This marking appears only on my commits -- others' commits
don't get pulled until there has been time for review. (I have to put
my commits somewhere, and maintaining two different branches would be
a real mess given the likelihood of depeendencies among comits.)
Thanx, Paul
------------------------------------------------------------------------
commit 49af6e403afab890a54518980d345431d74234a4
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Sat Feb 3 00:04:49 2018 -0800
EXP litmus_tests: Add comments explaining tests' purposes
This commit adds comments to the litmus tests summarizing what these
tests are intended to demonstrate.
Suggested-by: Ingo Molnar <mingo@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
index 5b83d57f6ac5..8e8ae8989085 100644
--- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoRR+poonceonce+Once
+(*
+ * Test of read-read coherence, that is, whether or not two successive
+ * reads from the same variable are ordered. They should be ordered,
+ * that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
index fab91c13d52c..0078ecd76f5e 100644
--- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoRW+poonceonce+Once
+(*
+ * Test of read-write coherence, that is, whether or not a read from a
+ * given variable followed by a write to that same variable are ordered.
+ * This should be ordered, that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
index 6a35ec2042ea..c9d342c8fbec 100644
--- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
@@ -1,5 +1,11 @@
C CoWR+poonceonce+Once
+(*
+ * Test of write-read coherence, that is, whether or not a write to a
+ * given variable followed by a read from that same variable are ordered.
+ * They should be ordered, that is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
index 32a96b832021..ad51c7b17f7b 100644
--- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
+++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
@@ -1,5 +1,11 @@
C CoWW+poonceonce
+(*
+ * Test of write-write coherence, that is, whether or not two successive
+ * writes to the same variable are ordered. They should be ordered, that
+ * is, this test should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
index 7eba2c68992b..8a58abce69fe 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
@@ -1,5 +1,14 @@
C IRIW+mbonceonces+OnceOnce
+(*
+ * Test of independent reads from independent writes with smp_mb()
+ * between each pairs of reads. In other words, is smp_mb() sufficient to
+ * cause two different reading processes to agree on the order of a pair
+ * of writes, where each write is to a different variable by a different
+ * process? The smp_mb()s should be sufficient, that is, this test should
+ * be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
index b0556c6c75d4..c736cd372207 100644
--- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
@@ -1,5 +1,14 @@
C IRIW+poonceonces+OnceOnce
+(*
+ * Test of independent reads from independent writes with nothing
+ * between each pairs of reads. In other words, is anything at all
+ * needed to cause two different reading processes to agree on the order
+ * of a pair of writes, where each write is to a different variable by a
+ * different process? Something is needed, in other words, this test
+ * should be allowed.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
index 9a1a233d70c3..1f1c4220c92d 100644
--- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
@@ -1,5 +1,13 @@
C ISA2+poonceonces
+(*
+ * Given a release-acquire chain ordering the first process's store
+ * against the last process's load, is ordering preserved if all of the
+ * smp_store_release() invocations be replaced by WRITE_ONCE() and all
+ * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
+ * The answer is "no", that is, this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
index 235195e87d4e..aa4b25838519 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
@@ -1,5 +1,14 @@
C ISA2+pooncerelease+poacquirerelease+poacquireonce
+(*
+ * This litmus test demonstrates that a release-acquire chain suffices
+ * to order P0()'s initial write against P2()'s final read. The reason
+ * that the release-acquire chain suffices is because in all but one
+ * case (P2() to P0()), each process reads from the preceding process's
+ * write. In memory-model-speak, there is only one non-reads-from
+ * (AKA non-rf) link, so release-acquire is all that is needed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
index dd5ac3a8974a..0b65048ad4db 100644
--- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
@@ -1,5 +1,14 @@
C LB+ctrlonceonce+mbonceonce
+(*
+ * This litmus test demonstrates that lightweight ordering suffices for
+ * the load-buffering pattern, in other words, preventing all processes
+ * reading from the preceding process's write. In this example, the
+ * combination of a control dependency and a full memory barrier are to do
+ * the trick. (But the full memory barrier could be replaced with another
+ * control dependency and order would still be maintained.)
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
index 47bd61319d93..1d1f45ff1940 100644
--- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
+++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
@@ -1,5 +1,12 @@
C LB+poacquireonce+pooncerelease
+(*
+ * Does a release-acquire pair suffice for the load-buffering litmus
+ * test, where each process reads from one of two variables then writes
+ * to the other? The answer is "yes", that is, this test should be
+ * forbidden.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
index a5cdf027e34b..383e3e0adb4e 100644
--- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
@@ -1,5 +1,11 @@
C LB+poonceonces
+(*
+ * Can the counter-intuitive outcome for the load-buffering pattern
+ * be prevented even with no explicit ordering? The answer should be
+ * "no", that is, this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 1a2fe5830381..86ddc88a26a2 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -1,5 +1,12 @@
C MP+onceassign+derefonce.litmus
+(*
+ * This litmus test demonstrates that rcu_assign_pointer() and
+ * rcu_dereference() suffice to ensure that an RCU reader will not see
+ * pre-initialization garbage when it traverses an RCU-protected data
+ * structure containing a newly inserted element.
+ *)
+
{
y=z;
z=0;
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 5fe6f1e3c452..3e5d3fe01054 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -1,5 +1,14 @@
C MP+polocks
+(*
+ * 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 relaasing a
+ * given lock), a CPU is not only guaranteed to see the accesses that other
+ * CPOs made while previously holding that lock, it are also guaranteed
+ * to see all prior accesses by those other CPUs.
+ *)
+
{}
P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 46e1ac7ba126..16a1d45e3fde 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -1,5 +1,11 @@
C MP+poonceonces
+(*
+ * Can the counter-intuitive message-passing outcome be prevented with
+ * no ordering at all? The answer should be "no", that is, this test
+ * should be prohibited.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index 0b00cc7293ba..f7fbe2636287 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -1,5 +1,11 @@
C MP+pooncerelease+poacquireonce
+(*
+ * This litmus test demonstrates that smp_store_release() and
+ * smp_load_acquire() provide sufficient ordering for the message-passing
+ * pattern.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 90d011c34f33..bd68debfaa95 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -1,5 +1,14 @@
C MP+porevlocks
+(*
+ * 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 relaasing a
+ * given lock), a CPU is not only guaranteed to see the accesses that other
+ * CPOs made while previously holding that lock, it are also guaranteed
+ * to see all prior accesses by those other CPUs.
+ *)
+
{}
P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
index 604ad41ea0c2..3d53ba138acd 100644
--- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
@@ -1,5 +1,11 @@
C MP+wmbonceonce+rmbonceonce
+(*
+ * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
+ * sufficient ordering for the message-passing pattern. However, it
+ * is usually better to use smp_store_release() and smp_load_acquire().
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
index e69b9e3e9436..4d64e547f1cd 100644
--- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
@@ -1,5 +1,12 @@
C R+mbonceonces
+(*
+ * This is the fully ordered (via smp_mb()) version of one of the classic
+ * counterintuitive litmus tests that illustrates the effects of store
+ * propagation delays. This test should be forbidden, but weaking either
+ * of the barriers would cause the resulting test to be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
index f7a12e00f82d..e75295b4e7c1 100644
--- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
@@ -1,5 +1,11 @@
C R+poonceonces
+(*
+ * This is the unordered (via smp_mb()) version of one of the classic
+ * counterintuitive litmus tests that illustrates the effects of store
+ * propagation delays. This test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
index d0d541c8ec7d..7fe16920a228 100644
--- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
@@ -1,5 +1,13 @@
C S+poonceonces
+(*
+ * Starting with a two-process release-acquire chain ordering P0()'s
+ * first store against P1()'s final load, if the smp_store_release()
+ * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
+ * READ_ONCE(), is ordering preserved. The answer is "of course not!",
+ * so this test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
index 1d292d0d6603..f78ce120863b 100644
--- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
@@ -1,5 +1,11 @@
C S+wmbonceonce+poacquireonce
+(*
+ * Can a smp_wmb(), instead of a release, and an acquire order a prior
+ * store against a subsequent store? The answer should be "yes", so
+ * this test should be forbidden.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
index b76caa5af1af..476542cd4a49 100644
--- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
@@ -1,5 +1,12 @@
C SB+mbonceonces
+(*
+ * This litmus test demonstrates that full memory barriers suffice to
+ * order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process read. (Locking and RCU can also
+ * suffice, but not much else.)
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
index c1797e03807e..40d519408ea6 100644
--- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
@@ -1,5 +1,11 @@
C SB+poonceonces
+(*
+ * This litmus test demonstrates that at least some ordering is required
+ * to order the store-buffering pattern, where each process writes to the
+ * variable that the preceding process read. This test should be allowed.
+ *)
+
{}
P0(int *x, int *y)
diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
index f5e7c92f61cc..0780a67cf3bd 100644
--- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -1,5 +1,11 @@
C WRC+poonceonces+Once
+(*
+ * This litmus test is an extension of the message-passing pattern, where
+ * the first write is moved to a separate process. But because this test
+ * has no ordering at all, it should be allowed.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
index e3d0018025dd..070166d435e5 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
@@ -1,5 +1,11 @@
C WRC+pooncerelease+rmbonceonce+Once
+(*
+ * This litmus test is an extension of the message-passing pattern, where
+ * the first write is moved to a separate process. Because it features
+ * a release and a read memory barrier, it should be forbidden.
+ *)
+
{}
P0(int *x)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
index 9c2cb53e6ef0..4d0a25665655 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
@@ -1,5 +1,12 @@
C Z6.0+pooncelock+poonceLock+pombonce
+(*
+ * This litmus test demonstrates how smp_mb__after_spinlock() may be
+ * used to ensure that accesses in different critical sections for a
+ * given lock running on different CPUs are nevertheless seen in order
+ * by CPUs not holding that lock.
+ *)
+
{}
P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
index c9a1f1a49ae1..8c723892716f 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
@@ -1,5 +1,11 @@
C Z6.0+pooncelock+pooncelock+pombonce
+(*
+ * This example demonstrates that a pair of accesses made by different
+ * processes each while holding a given lock will not necessarily be
+ * seen as ordered by a third process not holding that lock.
+ *)
+
{}
P0(int *x, int *y, spinlock_t *mylock)
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
index 25409a033514..8b0b1b3ca348 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
@@ -1,5 +1,17 @@
C Z6.0+pooncerelease+poacquirerelease+mbonceonce
+(*
+ * This litmus test shows that a release-acquire chain, while sufficient
+ * when there is but one non-reads-from (AKA non-rf) link, does not suffice
+ * if there is more than one. Of the three processes, only P1() reads from
+ * P0's write, which means that there are two non-rf links: P1() to P2()
+ * is a write-to-write link (AKA a "coherence" or just "co" link) and P2()
+ * to P0() is a read-to-write link (AKA a "from-reads" or just "fr" link).
+ * When there are two or more non-rf links, you typically will need one
+ * full barrier for each non-rf link. (Exceptions include some cases
+ * involving locking.)
+ *)
+
{}
P0(int *x, int *y)
^ permalink raw reply related [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-04 10:17 ` Paul E. McKenney
@ 2018-02-04 16:29 ` Andrea Parri
2018-02-05 5:00 ` Paul E. McKenney
2018-02-04 16:37 ` Alan Stern
1 sibling, 1 reply; 26+ messages in thread
From: Andrea Parri @ 2018-02-04 16:29 UTC (permalink / raw)
To: Paul E. McKenney
Cc: Alan Stern, Ingo Molnar, linux-kernel, linux-arch, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote:
[...]
> And here is the updated commit adding comments to the litmus test,
> which adds comments for the three litmus tests added above. I have also
> marked this commit with "EXP" indicating that it has not yet had time
> for review. This marking appears only on my commits -- others' commits
> don't get pulled until there has been time for review. (I have to put
> my commits somewhere, and maintaining two different branches would be
> a real mess given the likelihood of depeendencies among comits.)
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 49af6e403afab890a54518980d345431d74234a4
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date: Sat Feb 3 00:04:49 2018 -0800
>
> EXP litmus_tests: Add comments explaining tests' purposes
>
> This commit adds comments to the litmus tests summarizing what these
> tests are intended to demonstrate.
>
> Suggested-by: Ingo Molnar <mingo@kernel.org>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>
> diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> index 5b83d57f6ac5..8e8ae8989085 100644
> --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C CoRR+poonceonce+Once
>
> +(*
> + * Test of read-read coherence, that is, whether or not two successive
> + * reads from the same variable are ordered. They should be ordered,
> + * that is, this test should be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> index fab91c13d52c..0078ecd76f5e 100644
> --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C CoRW+poonceonce+Once
>
> +(*
> + * Test of read-write coherence, that is, whether or not a read from a
> + * given variable followed by a write to that same variable are ordered.
> + * This should be ordered, that is, this test should be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> index 6a35ec2042ea..c9d342c8fbec 100644
> --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C CoWR+poonceonce+Once
>
> +(*
> + * Test of write-read coherence, that is, whether or not a write to a
> + * given variable followed by a read from that same variable are ordered.
> + * They should be ordered, that is, this test should be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> index 32a96b832021..ad51c7b17f7b 100644
> --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> @@ -1,5 +1,11 @@
> C CoWW+poonceonce
>
> +(*
> + * Test of write-write coherence, that is, whether or not two successive
> + * writes to the same variable are ordered. They should be ordered, that
> + * is, this test should be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> index 7eba2c68992b..8a58abce69fe 100644
> --- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> @@ -1,5 +1,14 @@
> C IRIW+mbonceonces+OnceOnce
>
> +(*
> + * Test of independent reads from independent writes with smp_mb()
> + * between each pairs of reads. In other words, is smp_mb() sufficient to
> + * cause two different reading processes to agree on the order of a pair
> + * of writes, where each write is to a different variable by a different
> + * process? The smp_mb()s should be sufficient, that is, this test should
> + * be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> index b0556c6c75d4..c736cd372207 100644
> --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> @@ -1,5 +1,14 @@
> C IRIW+poonceonces+OnceOnce
>
> +(*
> + * Test of independent reads from independent writes with nothing
> + * between each pairs of reads. In other words, is anything at all
> + * needed to cause two different reading processes to agree on the order
> + * of a pair of writes, where each write is to a different variable by a
> + * different process? Something is needed, in other words, this test
> + * should be allowed.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> index 9a1a233d70c3..1f1c4220c92d 100644
> --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> @@ -1,5 +1,13 @@
> C ISA2+poonceonces
>
> +(*
> + * Given a release-acquire chain ordering the first process's store
> + * against the last process's load, is ordering preserved if all of the
> + * smp_store_release() invocations be replaced by WRITE_ONCE() and all
> + * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
> + * The answer is "no", that is, this test should be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> index 235195e87d4e..aa4b25838519 100644
> --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> @@ -1,5 +1,14 @@
> C ISA2+pooncerelease+poacquirerelease+poacquireonce
>
> +(*
> + * This litmus test demonstrates that a release-acquire chain suffices
> + * to order P0()'s initial write against P2()'s final read. The reason
> + * that the release-acquire chain suffices is because in all but one
> + * case (P2() to P0()), each process reads from the preceding process's
> + * write. In memory-model-speak, there is only one non-reads-from
> + * (AKA non-rf) link, so release-acquire is all that is needed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> index dd5ac3a8974a..0b65048ad4db 100644
> --- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> @@ -1,5 +1,14 @@
> C LB+ctrlonceonce+mbonceonce
>
> +(*
> + * This litmus test demonstrates that lightweight ordering suffices for
> + * the load-buffering pattern, in other words, preventing all processes
> + * reading from the preceding process's write. In this example, the
> + * combination of a control dependency and a full memory barrier are to do
> + * the trick. (But the full memory barrier could be replaced with another
> + * control dependency and order would still be maintained.)
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> index 47bd61319d93..1d1f45ff1940 100644
> --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> @@ -1,5 +1,12 @@
> C LB+poacquireonce+pooncerelease
>
> +(*
> + * Does a release-acquire pair suffice for the load-buffering litmus
> + * test, where each process reads from one of two variables then writes
> + * to the other? The answer is "yes", that is, this test should be
> + * forbidden.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> index a5cdf027e34b..383e3e0adb4e 100644
> --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C LB+poonceonces
>
> +(*
> + * Can the counter-intuitive outcome for the load-buffering pattern
> + * be prevented even with no explicit ordering? The answer should be
> + * "no", that is, this test should be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> index 1a2fe5830381..86ddc88a26a2 100644
> --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> @@ -1,5 +1,12 @@
> C MP+onceassign+derefonce.litmus
>
> +(*
> + * This litmus test demonstrates that rcu_assign_pointer() and
> + * rcu_dereference() suffice to ensure that an RCU reader will not see
> + * pre-initialization garbage when it traverses an RCU-protected data
> + * structure containing a newly inserted element.
> + *)
> +
> {
> y=z;
> z=0;
> diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
> index 5fe6f1e3c452..3e5d3fe01054 100644
> --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> @@ -1,5 +1,14 @@
> C MP+polocks
>
> +(*
> + * 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 relaasing a
s/relaasing/releasing
> + * given lock), a CPU is not only guaranteed to see the accesses that other
> + * CPOs made while previously holding that lock, it are also guaranteed
s/CPOs/CPUs
(same two typos for MP+porevlocks)
> + * to see all prior accesses by those other CPUs.
> + *)
> +
> {}
>
> P0(int *x, int *y, spinlock_t *mylock)
> diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> index 46e1ac7ba126..16a1d45e3fde 100644
> --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C MP+poonceonces
>
> +(*
> + * Can the counter-intuitive message-passing outcome be prevented with
> + * no ordering at all? The answer should be "no", that is, this test
> + * should be prohibited.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> index 0b00cc7293ba..f7fbe2636287 100644
> --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> @@ -1,5 +1,11 @@
> C MP+pooncerelease+poacquireonce
>
> +(*
> + * This litmus test demonstrates that smp_store_release() and
> + * smp_load_acquire() provide sufficient ordering for the message-passing
> + * pattern.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> index 90d011c34f33..bd68debfaa95 100644
> --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> @@ -1,5 +1,14 @@
> C MP+porevlocks
>
> +(*
> + * 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 relaasing a
> + * given lock), a CPU is not only guaranteed to see the accesses that other
> + * CPOs made while previously holding that lock, it are also guaranteed
> + * to see all prior accesses by those other CPUs.
> + *)
> +
> {}
>
> P0(int *x, int *y, spinlock_t *mylock)
> diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> index 604ad41ea0c2..3d53ba138acd 100644
> --- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> @@ -1,5 +1,11 @@
> C MP+wmbonceonce+rmbonceonce
>
> +(*
> + * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
> + * sufficient ordering for the message-passing pattern. However, it
> + * is usually better to use smp_store_release() and smp_load_acquire().
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> index e69b9e3e9436..4d64e547f1cd 100644
> --- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> @@ -1,5 +1,12 @@
> C R+mbonceonces
>
> +(*
> + * This is the fully ordered (via smp_mb()) version of one of the classic
> + * counterintuitive litmus tests that illustrates the effects of store
> + * propagation delays. This test should be forbidden, but weaking either
s/weaking/weakening
(ispell suggests so, at least ...)
Andrea
> + * of the barriers would cause the resulting test to be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> index f7a12e00f82d..e75295b4e7c1 100644
> --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C R+poonceonces
>
> +(*
> + * This is the unordered (via smp_mb()) version of one of the classic
> + * counterintuitive litmus tests that illustrates the effects of store
> + * propagation delays. This test should be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> index d0d541c8ec7d..7fe16920a228 100644
> --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> @@ -1,5 +1,13 @@
> C S+poonceonces
>
> +(*
> + * Starting with a two-process release-acquire chain ordering P0()'s
> + * first store against P1()'s final load, if the smp_store_release()
> + * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
> + * READ_ONCE(), is ordering preserved. The answer is "of course not!",
> + * so this test should be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> index 1d292d0d6603..f78ce120863b 100644
> --- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> @@ -1,5 +1,11 @@
> C S+wmbonceonce+poacquireonce
>
> +(*
> + * Can a smp_wmb(), instead of a release, and an acquire order a prior
> + * store against a subsequent store? The answer should be "yes", so
> + * this test should be forbidden.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> index b76caa5af1af..476542cd4a49 100644
> --- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> @@ -1,5 +1,12 @@
> C SB+mbonceonces
>
> +(*
> + * This litmus test demonstrates that full memory barriers suffice to
> + * order the store-buffering pattern, where each process writes to the
> + * variable that the preceding process read. (Locking and RCU can also
> + * suffice, but not much else.)
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> index c1797e03807e..40d519408ea6 100644
> --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C SB+poonceonces
>
> +(*
> + * This litmus test demonstrates that at least some ordering is required
> + * to order the store-buffering pattern, where each process writes to the
> + * variable that the preceding process read. This test should be allowed.
> + *)
> +
> {}
>
> P0(int *x, int *y)
> diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> index f5e7c92f61cc..0780a67cf3bd 100644
> --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> @@ -1,5 +1,11 @@
> C WRC+poonceonces+Once
>
> +(*
> + * This litmus test is an extension of the message-passing pattern, where
> + * the first write is moved to a separate process. But because this test
> + * has no ordering at all, it should be allowed.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> index e3d0018025dd..070166d435e5 100644
> --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C WRC+pooncerelease+rmbonceonce+Once
>
> +(*
> + * This litmus test is an extension of the message-passing pattern, where
> + * the first write is moved to a separate process. Because it features
> + * a release and a read memory barrier, it should be forbidden.
> + *)
> +
> {}
>
> P0(int *x)
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> index 9c2cb53e6ef0..4d0a25665655 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> @@ -1,5 +1,12 @@
> C Z6.0+pooncelock+poonceLock+pombonce
>
> +(*
> + * This litmus test demonstrates how smp_mb__after_spinlock() may be
> + * used to ensure that accesses in different critical sections for a
> + * given lock running on different CPUs are nevertheless seen in order
> + * by CPUs not holding that lock.
> + *)
> +
> {}
>
> P0(int *x, int *y, spinlock_t *mylock)
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> index c9a1f1a49ae1..8c723892716f 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> @@ -1,5 +1,11 @@
> C Z6.0+pooncelock+pooncelock+pombonce
>
> +(*
> + * This example demonstrates that a pair of accesses made by different
> + * processes each while holding a given lock will not necessarily be
> + * seen as ordered by a third process not holding that lock.
> + *)
> +
> {}
>
> P0(int *x, int *y, spinlock_t *mylock)
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> index 25409a033514..8b0b1b3ca348 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> @@ -1,5 +1,17 @@
> C Z6.0+pooncerelease+poacquirerelease+mbonceonce
>
> +(*
> + * This litmus test shows that a release-acquire chain, while sufficient
> + * when there is but one non-reads-from (AKA non-rf) link, does not suffice
> + * if there is more than one. Of the three processes, only P1() reads from
> + * P0's write, which means that there are two non-rf links: P1() to P2()
> + * is a write-to-write link (AKA a "coherence" or just "co" link) and P2()
> + * to P0() is a read-to-write link (AKA a "from-reads" or just "fr" link).
> + * When there are two or more non-rf links, you typically will need one
> + * full barrier for each non-rf link. (Exceptions include some cases
> + * involving locking.)
> + *)
> +
> {}
>
> P0(int *x, int *y)
>
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-04 10:17 ` Paul E. McKenney
2018-02-04 16:29 ` Andrea Parri
@ 2018-02-04 16:37 ` Alan Stern
2018-02-05 7:19 ` Paul E. McKenney
1 sibling, 1 reply; 26+ messages in thread
From: Alan Stern @ 2018-02-04 16:37 UTC (permalink / raw)
To: Paul E. McKenney
Cc: Ingo Molnar, linux-kernel, linux-arch, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sun, 4 Feb 2018, Paul E. McKenney wrote:
> --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C CoRW+poonceonce+Once
>
> +(*
> + * Test of read-write coherence, that is, whether or not a read from a
> + * given variable followed by a write to that same variable are ordered.
The syntax of this sentence is a little tortured. Suggestion:
... whether or not a read from a given variable and a later
write to that same variable are ordered.
> + * This should be ordered, that is, this test should be forbidden.
s/This/They/
> --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> @@ -1,5 +1,11 @@
> C CoWR+poonceonce+Once
>
> +(*
> + * Test of write-read coherence, that is, whether or not a write to a
> + * given variable followed by a read from that same variable are ordered.
Same syntax issue as above.
> --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> @@ -1,5 +1,13 @@
> C ISA2+poonceonces
>
> +(*
> + * Given a release-acquire chain ordering the first process's store
> + * against the last process's load, is ordering preserved if all of the
> + * smp_store_release() invocations be replaced by WRITE_ONCE() and all
s/be/are/
> + * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
s/be/are/
> --- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> @@ -1,5 +1,14 @@
> C LB+ctrlonceonce+mbonceonce
>
> +(*
> + * This litmus test demonstrates that lightweight ordering suffices for
> + * the load-buffering pattern, in other words, preventing all processes
> + * reading from the preceding process's write. In this example, the
> + * combination of a control dependency and a full memory barrier are to do
s/are to/are enough to/
> --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> @@ -1,5 +1,14 @@
> C MP+polocks
>
> +(*
> + * 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 relaasing a
s/relaasing/releasing/
> + * given lock), a CPU is not only guaranteed to see the accesses that other
> + * CPOs made while previously holding that lock, it are also guaranteed
s/CPO/CPU/
s/are/is/
> + * to see all prior accesses by those other CPUs.
Doesn't say whether the test should be allowed. This is true of several
other litmus tests too.
> --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> @@ -1,5 +1,14 @@
> C MP+porevlocks
>
> +(*
> + * 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 relaasing a
s/relaasing/releasing
> + * given lock), a CPU is not only guaranteed to see the accesses that other
> + * CPOs made while previously holding that lock, it are also guaranteed
s/CPO/CPU/
s/are/is/
> --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C R+poonceonces
>
> +(*
> + * This is the unordered (via smp_mb()) version of one of the classic
Does "unordered (via smp_mb())" mean that the test uses smp_mb() to
"unorder" the accesses, or does it mean that the test doesn't use smp_mb()
to order the accesses?
> --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> @@ -1,5 +1,13 @@
> C S+poonceonces
>
> +(*
> + * Starting with a two-process release-acquire chain ordering P0()'s
> + * first store against P1()'s final load, if the smp_store_release()
> + * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
> + * READ_ONCE(), is ordering preserved. The answer is "of course not!",
s/./?/
> --- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> @@ -1,5 +1,12 @@
> C SB+mbonceonces
>
> +(*
> + * This litmus test demonstrates that full memory barriers suffice to
> + * order the store-buffering pattern, where each process writes to the
> + * variable that the preceding process read. (Locking and RCU can also
s/read/reads/
> --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> @@ -1,5 +1,11 @@
> C SB+poonceonces
>
> +(*
> + * This litmus test demonstrates that at least some ordering is required
> + * to order the store-buffering pattern, where each process writes to the
> + * variable that the preceding process read. This test should be allowed.
s/read/reads/
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> @@ -1,5 +1,11 @@
> C Z6.0+pooncelock+pooncelock+pombonce
>
> +(*
> + * This example demonstrates that a pair of accesses made by different
> + * processes each while holding a given lock will not necessarily be
> + * seen as ordered by a third process not holding that lock.
> + *)
Note that the outcome of this test will be changed by one of the
patches in our "pending" list.
Alan
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-04 16:29 ` Andrea Parri
@ 2018-02-05 5:00 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-05 5:00 UTC (permalink / raw)
To: Andrea Parri
Cc: Alan Stern, Ingo Molnar, linux-kernel, linux-arch, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sun, Feb 04, 2018 at 05:29:00PM +0100, Andrea Parri wrote:
> On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote:
>
> [...]
>
> > And here is the updated commit adding comments to the litmus test,
> > which adds comments for the three litmus tests added above. I have also
> > marked this commit with "EXP" indicating that it has not yet had time
> > for review. This marking appears only on my commits -- others' commits
> > don't get pulled until there has been time for review. (I have to put
> > my commits somewhere, and maintaining two different branches would be
> > a real mess given the likelihood of depeendencies among comits.)
> >
> > Thanx, Paul
> >
> > ------------------------------------------------------------------------
> >
> > commit 49af6e403afab890a54518980d345431d74234a4
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date: Sat Feb 3 00:04:49 2018 -0800
> >
> > EXP litmus_tests: Add comments explaining tests' purposes
> >
> > This commit adds comments to the litmus tests summarizing what these
> > tests are intended to demonstrate.
> >
> > Suggested-by: Ingo Molnar <mingo@kernel.org>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >
> > diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > index 5b83d57f6ac5..8e8ae8989085 100644
> > --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C CoRR+poonceonce+Once
> >
> > +(*
> > + * Test of read-read coherence, that is, whether or not two successive
> > + * reads from the same variable are ordered. They should be ordered,
> > + * that is, this test should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > index fab91c13d52c..0078ecd76f5e 100644
> > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C CoRW+poonceonce+Once
> >
> > +(*
> > + * Test of read-write coherence, that is, whether or not a read from a
> > + * given variable followed by a write to that same variable are ordered.
> > + * This should be ordered, that is, this test should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > index 6a35ec2042ea..c9d342c8fbec 100644
> > --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C CoWR+poonceonce+Once
> >
> > +(*
> > + * Test of write-read coherence, that is, whether or not a write to a
> > + * given variable followed by a read from that same variable are ordered.
> > + * They should be ordered, that is, this test should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > index 32a96b832021..ad51c7b17f7b 100644
> > --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > @@ -1,5 +1,11 @@
> > C CoWW+poonceonce
> >
> > +(*
> > + * Test of write-write coherence, that is, whether or not two successive
> > + * writes to the same variable are ordered. They should be ordered, that
> > + * is, this test should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> > index 7eba2c68992b..8a58abce69fe 100644
> > --- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> > +++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> > @@ -1,5 +1,14 @@
> > C IRIW+mbonceonces+OnceOnce
> >
> > +(*
> > + * Test of independent reads from independent writes with smp_mb()
> > + * between each pairs of reads. In other words, is smp_mb() sufficient to
> > + * cause two different reading processes to agree on the order of a pair
> > + * of writes, where each write is to a different variable by a different
> > + * process? The smp_mb()s should be sufficient, that is, this test should
> > + * be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > index b0556c6c75d4..c736cd372207 100644
> > --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > @@ -1,5 +1,14 @@
> > C IRIW+poonceonces+OnceOnce
> >
> > +(*
> > + * Test of independent reads from independent writes with nothing
> > + * between each pairs of reads. In other words, is anything at all
> > + * needed to cause two different reading processes to agree on the order
> > + * of a pair of writes, where each write is to a different variable by a
> > + * different process? Something is needed, in other words, this test
> > + * should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > index 9a1a233d70c3..1f1c4220c92d 100644
> > --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > @@ -1,5 +1,13 @@
> > C ISA2+poonceonces
> >
> > +(*
> > + * Given a release-acquire chain ordering the first process's store
> > + * against the last process's load, is ordering preserved if all of the
> > + * smp_store_release() invocations be replaced by WRITE_ONCE() and all
> > + * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
> > + * The answer is "no", that is, this test should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > index 235195e87d4e..aa4b25838519 100644
> > --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > @@ -1,5 +1,14 @@
> > C ISA2+pooncerelease+poacquirerelease+poacquireonce
> >
> > +(*
> > + * This litmus test demonstrates that a release-acquire chain suffices
> > + * to order P0()'s initial write against P2()'s final read. The reason
> > + * that the release-acquire chain suffices is because in all but one
> > + * case (P2() to P0()), each process reads from the preceding process's
> > + * write. In memory-model-speak, there is only one non-reads-from
> > + * (AKA non-rf) link, so release-acquire is all that is needed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > index dd5ac3a8974a..0b65048ad4db 100644
> > --- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > @@ -1,5 +1,14 @@
> > C LB+ctrlonceonce+mbonceonce
> >
> > +(*
> > + * This litmus test demonstrates that lightweight ordering suffices for
> > + * the load-buffering pattern, in other words, preventing all processes
> > + * reading from the preceding process's write. In this example, the
> > + * combination of a control dependency and a full memory barrier are to do
> > + * the trick. (But the full memory barrier could be replaced with another
> > + * control dependency and order would still be maintained.)
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > index 47bd61319d93..1d1f45ff1940 100644
> > --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > @@ -1,5 +1,12 @@
> > C LB+poacquireonce+pooncerelease
> >
> > +(*
> > + * Does a release-acquire pair suffice for the load-buffering litmus
> > + * test, where each process reads from one of two variables then writes
> > + * to the other? The answer is "yes", that is, this test should be
> > + * forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > index a5cdf027e34b..383e3e0adb4e 100644
> > --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C LB+poonceonces
> >
> > +(*
> > + * Can the counter-intuitive outcome for the load-buffering pattern
> > + * be prevented even with no explicit ordering? The answer should be
> > + * "no", that is, this test should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > index 1a2fe5830381..86ddc88a26a2 100644
> > --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > @@ -1,5 +1,12 @@
> > C MP+onceassign+derefonce.litmus
> >
> > +(*
> > + * This litmus test demonstrates that rcu_assign_pointer() and
> > + * rcu_dereference() suffice to ensure that an RCU reader will not see
> > + * pre-initialization garbage when it traverses an RCU-protected data
> > + * structure containing a newly inserted element.
> > + *)
> > +
> > {
> > y=z;
> > z=0;
> > diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
> > index 5fe6f1e3c452..3e5d3fe01054 100644
> > --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> > @@ -1,5 +1,14 @@
> > C MP+polocks
> >
> > +(*
> > + * 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 relaasing a
>
> s/relaasing/releasing
>
>
> > + * given lock), a CPU is not only guaranteed to see the accesses that other
> > + * CPOs made while previously holding that lock, it are also guaranteed
>
> s/CPOs/CPUs
>
> (same two typos for MP+porevlocks)
Good eyes, fixed in both files.
> > + * to see all prior accesses by those other CPUs.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y, spinlock_t *mylock)
> > diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > index 46e1ac7ba126..16a1d45e3fde 100644
> > --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C MP+poonceonces
> >
> > +(*
> > + * Can the counter-intuitive message-passing outcome be prevented with
> > + * no ordering at all? The answer should be "no", that is, this test
> > + * should be prohibited.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > index 0b00cc7293ba..f7fbe2636287 100644
> > --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > @@ -1,5 +1,11 @@
> > C MP+pooncerelease+poacquireonce
> >
> > +(*
> > + * This litmus test demonstrates that smp_store_release() and
> > + * smp_load_acquire() provide sufficient ordering for the message-passing
> > + * pattern.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > index 90d011c34f33..bd68debfaa95 100644
> > --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > @@ -1,5 +1,14 @@
> > C MP+porevlocks
> >
> > +(*
> > + * 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 relaasing a
> > + * given lock), a CPU is not only guaranteed to see the accesses that other
> > + * CPOs made while previously holding that lock, it are also guaranteed
> > + * to see all prior accesses by those other CPUs.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y, spinlock_t *mylock)
> > diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> > index 604ad41ea0c2..3d53ba138acd 100644
> > --- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> > @@ -1,5 +1,11 @@
> > C MP+wmbonceonce+rmbonceonce
> >
> > +(*
> > + * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
> > + * sufficient ordering for the message-passing pattern. However, it
> > + * is usually better to use smp_store_release() and smp_load_acquire().
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> > index e69b9e3e9436..4d64e547f1cd 100644
> > --- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus
> > @@ -1,5 +1,12 @@
> > C R+mbonceonces
> >
> > +(*
> > + * This is the fully ordered (via smp_mb()) version of one of the classic
> > + * counterintuitive litmus tests that illustrates the effects of store
> > + * propagation delays. This test should be forbidden, but weaking either
>
> s/weaking/weakening
>
> (ispell suggests so, at least ...)
I agree with ispell, thank you! ;-)
Thanx, Paul
> Andrea
>
>
> > + * of the barriers would cause the resulting test to be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > index f7a12e00f82d..e75295b4e7c1 100644
> > --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C R+poonceonces
> >
> > +(*
> > + * This is the unordered (via smp_mb()) version of one of the classic
> > + * counterintuitive litmus tests that illustrates the effects of store
> > + * propagation delays. This test should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > index d0d541c8ec7d..7fe16920a228 100644
> > --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > @@ -1,5 +1,13 @@
> > C S+poonceonces
> >
> > +(*
> > + * Starting with a two-process release-acquire chain ordering P0()'s
> > + * first store against P1()'s final load, if the smp_store_release()
> > + * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
> > + * READ_ONCE(), is ordering preserved. The answer is "of course not!",
> > + * so this test should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> > index 1d292d0d6603..f78ce120863b 100644
> > --- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> > @@ -1,5 +1,11 @@
> > C S+wmbonceonce+poacquireonce
> >
> > +(*
> > + * Can a smp_wmb(), instead of a release, and an acquire order a prior
> > + * store against a subsequent store? The answer should be "yes", so
> > + * this test should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > index b76caa5af1af..476542cd4a49 100644
> > --- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > @@ -1,5 +1,12 @@
> > C SB+mbonceonces
> >
> > +(*
> > + * This litmus test demonstrates that full memory barriers suffice to
> > + * order the store-buffering pattern, where each process writes to the
> > + * variable that the preceding process read. (Locking and RCU can also
> > + * suffice, but not much else.)
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > index c1797e03807e..40d519408ea6 100644
> > --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C SB+poonceonces
> >
> > +(*
> > + * This litmus test demonstrates that at least some ordering is required
> > + * to order the store-buffering pattern, where each process writes to the
> > + * variable that the preceding process read. This test should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> > diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > index f5e7c92f61cc..0780a67cf3bd 100644
> > --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > @@ -1,5 +1,11 @@
> > C WRC+poonceonces+Once
> >
> > +(*
> > + * This litmus test is an extension of the message-passing pattern, where
> > + * the first write is moved to a separate process. But because this test
> > + * has no ordering at all, it should be allowed.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> > index e3d0018025dd..070166d435e5 100644
> > --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C WRC+pooncerelease+rmbonceonce+Once
> >
> > +(*
> > + * This litmus test is an extension of the message-passing pattern, where
> > + * the first write is moved to a separate process. Because it features
> > + * a release and a read memory barrier, it should be forbidden.
> > + *)
> > +
> > {}
> >
> > P0(int *x)
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > index 9c2cb53e6ef0..4d0a25665655 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > @@ -1,5 +1,12 @@
> > C Z6.0+pooncelock+poonceLock+pombonce
> >
> > +(*
> > + * This litmus test demonstrates how smp_mb__after_spinlock() may be
> > + * used to ensure that accesses in different critical sections for a
> > + * given lock running on different CPUs are nevertheless seen in order
> > + * by CPUs not holding that lock.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y, spinlock_t *mylock)
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > index c9a1f1a49ae1..8c723892716f 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > @@ -1,5 +1,11 @@
> > C Z6.0+pooncelock+pooncelock+pombonce
> >
> > +(*
> > + * This example demonstrates that a pair of accesses made by different
> > + * processes each while holding a given lock will not necessarily be
> > + * seen as ordered by a third process not holding that lock.
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y, spinlock_t *mylock)
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> > index 25409a033514..8b0b1b3ca348 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> > @@ -1,5 +1,17 @@
> > C Z6.0+pooncerelease+poacquirerelease+mbonceonce
> >
> > +(*
> > + * This litmus test shows that a release-acquire chain, while sufficient
> > + * when there is but one non-reads-from (AKA non-rf) link, does not suffice
> > + * if there is more than one. Of the three processes, only P1() reads from
> > + * P0's write, which means that there are two non-rf links: P1() to P2()
> > + * is a write-to-write link (AKA a "coherence" or just "co" link) and P2()
> > + * to P0() is a read-to-write link (AKA a "from-reads" or just "fr" link).
> > + * When there are two or more non-rf links, you typically will need one
> > + * full barrier for each non-rf link. (Exceptions include some cases
> > + * involving locking.)
> > + *)
> > +
> > {}
> >
> > P0(int *x, int *y)
> >
>
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-04 16:37 ` Alan Stern
@ 2018-02-05 7:19 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-05 7:19 UTC (permalink / raw)
To: Alan Stern
Cc: Ingo Molnar, linux-kernel, linux-arch, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks, Thomas Gleixner, Peter Zijlstra,
Linus Torvalds
On Sun, Feb 04, 2018 at 11:37:59AM -0500, Alan Stern wrote:
> On Sun, 4 Feb 2018, Paul E. McKenney wrote:
>
> > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C CoRW+poonceonce+Once
> >
> > +(*
> > + * Test of read-write coherence, that is, whether or not a read from a
> > + * given variable followed by a write to that same variable are ordered.
>
> The syntax of this sentence is a little tortured. Suggestion:
>
> ... whether or not a read from a given variable and a later
> write to that same variable are ordered.
>
> > + * This should be ordered, that is, this test should be forbidden.
>
> s/This/They/
Good catches, both changed as suggested.
> > --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > @@ -1,5 +1,11 @@
> > C CoWR+poonceonce+Once
> >
> > +(*
> > + * Test of write-read coherence, that is, whether or not a write to a
> > + * given variable followed by a read from that same variable are ordered.
>
> Same syntax issue as above.
Analogous fixed applied!
> > --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > @@ -1,5 +1,13 @@
> > C ISA2+poonceonces
> >
> > +(*
> > + * Given a release-acquire chain ordering the first process's store
> > + * against the last process's load, is ordering preserved if all of the
> > + * smp_store_release() invocations be replaced by WRITE_ONCE() and all
>
> s/be/are/
>
> > + * of the smp_load_acquire() invocations be replaced by READ_ONCE()?
>
> s/be/are/
Good eyes, fixed!
> > --- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > @@ -1,5 +1,14 @@
> > C LB+ctrlonceonce+mbonceonce
> >
> > +(*
> > + * This litmus test demonstrates that lightweight ordering suffices for
> > + * the load-buffering pattern, in other words, preventing all processes
> > + * reading from the preceding process's write. In this example, the
> > + * combination of a control dependency and a full memory barrier are to do
>
> s/are to/are enough to/
Ditto!
> > --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> > @@ -1,5 +1,14 @@
> > C MP+polocks
> >
> > +(*
> > + * 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 relaasing a
>
> s/relaasing/releasing/
>
> > + * given lock), a CPU is not only guaranteed to see the accesses that other
> > + * CPOs made while previously holding that lock, it are also guaranteed
>
> s/CPO/CPU/
> s/are/is/
Andrea beat you to the first two of these three, but fixed. ;-)
> > + * to see all prior accesses by those other CPUs.
>
> Doesn't say whether the test should be allowed. This is true of several
> other litmus tests too.
Added the "Forbidden".
You know, I should use the machine-generated syntax that my scripts
recognize, shouldn't I? Doing that as well.
> > --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > @@ -1,5 +1,14 @@
> > C MP+porevlocks
> >
> > +(*
> > + * 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 relaasing a
>
> s/relaasing/releasing
>
> > + * given lock), a CPU is not only guaranteed to see the accesses that other
> > + * CPOs made while previously holding that lock, it are also guaranteed
>
> s/CPO/CPU/
> s/are/is/
Fixed!
> > --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C R+poonceonces
> >
> > +(*
> > + * This is the unordered (via smp_mb()) version of one of the classic
>
> Does "unordered (via smp_mb())" mean that the test uses smp_mb() to
> "unorder" the accesses, or does it mean that the test doesn't use smp_mb()
> to order the accesses?
That is a bit ambiguous... Though I would be interested in seeing a
litmus test that really did use smp_mb() to unorder the accesses!
How about the following?
* Result: Sometimes
*
* This is the unordered (thus lacking smp_mb()) version of one of the
* classic counterintuitive litmus tests that illustrates the effects of
* store propagation delays.
> > --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > @@ -1,5 +1,13 @@
> > C S+poonceonces
> >
> > +(*
> > + * Starting with a two-process release-acquire chain ordering P0()'s
> > + * first store against P1()'s final load, if the smp_store_release()
> > + * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
> > + * READ_ONCE(), is ordering preserved. The answer is "of course not!",
>
> s/./?/
Good eyes, fixed!
> > --- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > @@ -1,5 +1,12 @@
> > C SB+mbonceonces
> >
> > +(*
> > + * This litmus test demonstrates that full memory barriers suffice to
> > + * order the store-buffering pattern, where each process writes to the
> > + * variable that the preceding process read. (Locking and RCU can also
>
> s/read/reads/
Ditto!
> > --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > @@ -1,5 +1,11 @@
> > C SB+poonceonces
> >
> > +(*
> > + * This litmus test demonstrates that at least some ordering is required
> > + * to order the store-buffering pattern, where each process writes to the
> > + * variable that the preceding process read. This test should be allowed.
>
> s/read/reads/
And ditto again! (Hey, at least I was consistent! If you didn't know
better, you might even think that I was using copy-and-paste.)
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > @@ -1,5 +1,11 @@
> > C Z6.0+pooncelock+pooncelock+pombonce
> >
> > +(*
> > + * This example demonstrates that a pair of accesses made by different
> > + * processes each while holding a given lock will not necessarily be
> > + * seen as ordered by a third process not holding that lock.
> > + *)
>
> Note that the outcome of this test will be changed by one of the
> patches in our "pending" list.
I decided to anticipate that change and marked it "Result: Never". ;-)
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-01-25 9:34 [GIT PULL tools] Linux kernel memory model Paul E. McKenney
2018-01-29 6:57 ` Ingo Molnar
@ 2018-02-08 18:41 ` Patrick Bellasi
2018-02-08 20:02 ` Peter Zijlstra
2018-02-09 11:33 ` Paul E. McKenney
1 sibling, 2 replies; 26+ messages in thread
From: Patrick Bellasi @ 2018-02-08 18:41 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks
Hi Paul,
thanks to you and all the involved guys for this useful tool.
I give it a try today and found that by installing herd7 by just
following the instruction in herdtools7/INSTALL.md, and precisely
installing it via:
opam install herdtools7
it seems to give you a tool which fails to run the basic example in
your README with this error:
File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
everything works fine.
Maybe it's a know issue, in case just ignore me. :)
Otherwise, maybe it can be worth to add to the README a note on which
minimum version of the herd7 tool is required.
opma version (not working) : 7.47, Rev: exported
master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
Cheers Patrick
On 25-Jan 01:34, Paul E. McKenney wrote:
> Hello, Ingo,
>
> This pull request contains a single commit that adds a memory model to
> the tools directory. This memory model can (roughly speaking) be thought
> of as an automated version of memory-barriers.txt. It is written in the
> "cat" language, which is executable by the externally provided "herd7"
> simulator, which exhaustively explores the state space of small litmus
> tests.
>
> This memory model is accompanied by extensive documentation on its use
> and its design. Two versions have been sent to LKML and feedback
> incorporated:
>
> 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
>
> This model has been presented and demoed at a number of Linux gatherings,
> including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> Plumbers Conference, which featured a workshop helping a number of Linux
> kernel hackers install and use the tool.
>
> This memory model has matured to the point where it would be good to include
> it in the Linux kernel, for example, to allow it to track changes as new
> hardware and use cases are added. We expect the rate of change to be similar
> to that of Documentation/memory-barriers.txt.
>
> This memory model is available in the git repository at:
>
> git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
>
> for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
>
> Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
>
> ----------------------------------------------------------------
> Paul E. McKenney (1):
> Automate memory-barriers.txt; provide Linux-kernel memory model
>
> tools/memory-model/Documentation/cheatsheet.txt | 30 +
> tools/memory-model/Documentation/explanation.txt | 1840 ++++++++++++++++++++
> tools/memory-model/Documentation/recipes.txt | 570 ++++++
> tools/memory-model/Documentation/references.txt | 107 ++
> tools/memory-model/MAINTAINERS | 15 +
> tools/memory-model/README | 220 +++
> tools/memory-model/linux-kernel.bell | 53 +
> tools/memory-model/linux-kernel.cat | 124 ++
> tools/memory-model/linux-kernel.cfg | 21 +
> tools/memory-model/linux-kernel.def | 108 ++
> .../litmus-tests/CoRR+poonceonce+Once.litmus | 19 +
> .../litmus-tests/CoRW+poonceonce+Once.litmus | 18 +
> .../litmus-tests/CoWR+poonceonce+Once.litmus | 18 +
> .../litmus-tests/CoWW+poonceonce.litmus | 11 +
> .../litmus-tests/IRIW+mbonceonces+OnceOnce.litmus | 35 +
> .../litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 33 +
> .../litmus-tests/ISA2+poonceonces.litmus | 28 +
> ...cerelease+poacquirerelease+poacquireonce.litmus | 28 +
> .../litmus-tests/LB+ctrlonceonce+mbonceonce.litmus | 23 +
> .../LB+poacquireonce+pooncerelease.litmus | 21 +
> .../litmus-tests/LB+poonceonces.litmus | 21 +
> .../litmus-tests/MP+onceassign+derefonce.litmus | 25 +
> tools/memory-model/litmus-tests/MP+polocks.litmus | 24 +
> .../litmus-tests/MP+poonceonces.litmus | 20 +
> .../MP+pooncerelease+poacquireonce.litmus | 20 +
> .../memory-model/litmus-tests/MP+porevlocks.litmus | 24 +
> .../litmus-tests/MP+wmbonceonce+rmbonceonce.litmus | 22 +
> .../memory-model/litmus-tests/R+mbonceonces.litmus | 21 +
> .../memory-model/litmus-tests/R+poonceonces.litmus | 19 +
> tools/memory-model/litmus-tests/README | 125 ++
> .../memory-model/litmus-tests/S+poonceonces.litmus | 19 +
> .../S+wmbonceonce+poacquireonce.litmus | 20 +
> .../litmus-tests/SB+mbonceonces.litmus | 23 +
> .../litmus-tests/SB+poonceonces.litmus | 21 +
> .../litmus-tests/WRC+poonceonces+Once.litmus | 27 +
> .../WRC+pooncerelease+rmbonceonce+Once.litmus | 28 +
> .../Z6.0+pooncelock+poonceLock+pombonce.litmus | 33 +
> .../Z6.0+pooncelock+pooncelock+pombonce.litmus | 32 +
> ...ooncerelease+poacquirerelease+mbonceonce.litmus | 28 +
> tools/memory-model/lock.cat | 99 ++
> 40 files changed, 3973 insertions(+)
> create mode 100644 tools/memory-model/Documentation/cheatsheet.txt
> create mode 100644 tools/memory-model/Documentation/explanation.txt
> create mode 100644 tools/memory-model/Documentation/recipes.txt
> create mode 100644 tools/memory-model/Documentation/references.txt
> create mode 100644 tools/memory-model/MAINTAINERS
> create mode 100644 tools/memory-model/README
> create mode 100644 tools/memory-model/linux-kernel.bell
> create mode 100644 tools/memory-model/linux-kernel.cat
> create mode 100644 tools/memory-model/linux-kernel.cfg
> create mode 100644 tools/memory-model/linux-kernel.def
> create mode 100644 tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> create mode 100644 tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> create mode 100644 tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> create mode 100644 tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> create mode 100644 tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> create mode 100644 tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> create mode 100644 tools/memory-model/litmus-tests/LB+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+polocks.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+porevlocks.litmus
> create mode 100644 tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/R+mbonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/R+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/README
> create mode 100644 tools/memory-model/litmus-tests/S+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/SB+poonceonces.litmus
> create mode 100644 tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> create mode 100644 tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> create mode 100644 tools/memory-model/lock.cat
>
--
#include <best/regards.h>
Patrick Bellasi
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-08 18:41 ` Patrick Bellasi
@ 2018-02-08 20:02 ` Peter Zijlstra
2018-02-09 9:11 ` Andrea Parri
2018-02-09 11:33 ` Paul E. McKenney
1 sibling, 1 reply; 26+ messages in thread
From: Peter Zijlstra @ 2018-02-08 20:02 UTC (permalink / raw)
To: Patrick Bellasi
Cc: Paul E. McKenney, linux-kernel, linux-arch, stern, parri.andrea,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks
On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> Hi Paul,
> thanks to you and all the involved guys for this useful tool.
>
> I give it a try today and found that by installing herd7 by just
> following the instruction in herdtools7/INSTALL.md, and precisely
> installing it via:
>
> opam install herdtools7
>
> it seems to give you a tool which fails to run the basic example in
> your README with this error:
>
> File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
>
> As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> everything works fine.
>
> Maybe it's a know issue, in case just ignore me. :)
>
> Otherwise, maybe it can be worth to add to the README a note on which
> minimum version of the herd7 tool is required.
>
> opma version (not working) : 7.47, Rev: exported
> master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
Urgh. So that's why it wouldn't work.
I remember Paul saying you needed the latest version, which is why I
rebuild from opam, but building top of git is a bit much.
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-08 20:02 ` Peter Zijlstra
@ 2018-02-09 9:11 ` Andrea Parri
2018-02-09 11:29 ` Paul E. McKenney
0 siblings, 1 reply; 26+ messages in thread
From: Andrea Parri @ 2018-02-09 9:11 UTC (permalink / raw)
To: Peter Zijlstra
Cc: Patrick Bellasi, Paul E. McKenney, linux-kernel, linux-arch,
stern, j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks
On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote:
> On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> > Hi Paul,
> > thanks to you and all the involved guys for this useful tool.
> >
> > I give it a try today and found that by installing herd7 by just
> > following the instruction in herdtools7/INSTALL.md, and precisely
> > installing it via:
> >
> > opam install herdtools7
> >
> > it seems to give you a tool which fails to run the basic example in
> > your README with this error:
> >
> > File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
> >
> > As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> > everything works fine.
> >
> > Maybe it's a know issue, in case just ignore me. :)
> >
> > Otherwise, maybe it can be worth to add to the README a note on which
> > minimum version of the herd7 tool is required.
> >
> > opma version (not working) : 7.47, Rev: exported
> > master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
>
> Urgh. So that's why it wouldn't work.
>
> I remember Paul saying you needed the latest version, which is why I
> rebuild from opam, but building top of git is a bit much.
+1
_Sadly_ enough, co-developers and I were aware of this issue,
but it was only mildly reported here (c.f.,
https://marc.info/?l=linux-kernel&m=151638196427685&w=2 ).
This bisects to that (crazy):
2d5fba7782d669c6a1cc577dbc3bf507780273bb
("linux-kernel*: Make RCU identifiers match ASPLOS paper")
From repo.: https://github.com/aparri/memory-model
which not only did break 7.47, but also made the bell uglier
by mixing dashes and underscores in a very same block.
As a solution to this issue, I can envisage a partial revert
of that commit (just replace those dashes); Paul, Jade, Luc:
any better solution?
(Sorry for being late on IRC, glad this came out here,)
Andrea
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-09 9:11 ` Andrea Parri
@ 2018-02-09 11:29 ` Paul E. McKenney
2018-02-09 12:41 ` Andrea Parri
0 siblings, 1 reply; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-09 11:29 UTC (permalink / raw)
To: Andrea Parri
Cc: Peter Zijlstra, Patrick Bellasi, linux-kernel, linux-arch, stern,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks
On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote:
> On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote:
> > On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> > > Hi Paul,
> > > thanks to you and all the involved guys for this useful tool.
> > >
> > > I give it a try today and found that by installing herd7 by just
> > > following the instruction in herdtools7/INSTALL.md, and precisely
> > > installing it via:
> > >
> > > opam install herdtools7
> > >
> > > it seems to give you a tool which fails to run the basic example in
> > > your README with this error:
> > >
> > > File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
> > >
> > > As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> > > everything works fine.
> > >
> > > Maybe it's a know issue, in case just ignore me. :)
> > >
> > > Otherwise, maybe it can be worth to add to the README a note on which
> > > minimum version of the herd7 tool is required.
> > >
> > > opma version (not working) : 7.47, Rev: exported
> > > master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
> >
> > Urgh. So that's why it wouldn't work.
> >
> > I remember Paul saying you needed the latest version, which is why I
> > rebuild from opam, but building top of git is a bit much.
>
> +1
>
> _Sadly_ enough, co-developers and I were aware of this issue,
> but it was only mildly reported here (c.f.,
>
> https://marc.info/?l=linux-kernel&m=151638196427685&w=2 ).
>
> This bisects to that (crazy):
>
> 2d5fba7782d669c6a1cc577dbc3bf507780273bb
> ("linux-kernel*: Make RCU identifiers match ASPLOS paper")
>
> From repo.: https://github.com/aparri/memory-model
>
> which not only did break 7.47, but also made the bell uglier
> by mixing dashes and underscores in a very same block.
>
> As a solution to this issue, I can envisage a partial revert
> of that commit (just replace those dashes); Paul, Jade, Luc:
> any better solution?
>
> (Sorry for being late on IRC, glad this came out here,)
Or maybe a 7.48 release?
Thanx, Paul
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-08 18:41 ` Patrick Bellasi
2018-02-08 20:02 ` Peter Zijlstra
@ 2018-02-09 11:33 ` Paul E. McKenney
1 sibling, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-09 11:33 UTC (permalink / raw)
To: Patrick Bellasi
Cc: linux-kernel, linux-arch, stern, parri.andrea, j.alglave,
luc.maranget, boqun.feng, will.deacon, peterz, npiggin, dhowells,
elena.reshetova, mhocko, akiyks
On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> Hi Paul,
> thanks to you and all the involved guys for this useful tool.
>
> I give it a try today and found that by installing herd7 by just
> following the instruction in herdtools7/INSTALL.md, and precisely
> installing it via:
>
> opam install herdtools7
>
> it seems to give you a tool which fails to run the basic example in
> your README with this error:
>
> File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
>
> As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> everything works fine.
>
> Maybe it's a know issue, in case just ignore me. :)
>
> Otherwise, maybe it can be worth to add to the README a note on which
> minimum version of the herd7 tool is required.
>
> opma version (not working) : 7.47, Rev: exported
> master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
Thank you for trying it out, and apologies for the hassle!
These sort of "flag day" updates have happened from time to time due to
the occasional need to have coordinated updates adding features to herd7
to enable new features in LKMM. As Andrea pointed out, this particular
flag day could be argued to be a bit less necessary than most, and again,
apologies for the hassle.
We will get this straightened out one way or another...
Thanx, Paul
> Cheers Patrick
>
> On 25-Jan 01:34, Paul E. McKenney wrote:
> > Hello, Ingo,
> >
> > This pull request contains a single commit that adds a memory model to
> > the tools directory. This memory model can (roughly speaking) be thought
> > of as an automated version of memory-barriers.txt. It is written in the
> > "cat" language, which is executable by the externally provided "herd7"
> > simulator, which exhaustively explores the state space of small litmus
> > tests.
> >
> > This memory model is accompanied by extensive documentation on its use
> > and its design. Two versions have been sent to LKML and feedback
> > incorporated:
> >
> > 1. http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com
> > 2. http://lkml.kernel.org/r/20180119035855.GA29296@linux.vnet.ibm.com
> >
> > This model has been presented and demoed at a number of Linux gatherings,
> > including the 2016 LinuxCon EU, the 2016 Linux Plumbers Conference,
> > the 2016 Linux Kernel Summit, the 2017 linux.conf.au, and the 2017 Linux
> > Plumbers Conference, which featured a workshop helping a number of Linux
> > kernel hackers install and use the tool.
> >
> > This memory model has matured to the point where it would be good to include
> > it in the Linux kernel, for example, to allow it to track changes as new
> > hardware and use cases are added. We expect the rate of change to be similar
> > to that of Documentation/memory-barriers.txt.
> >
> > This memory model is available in the git repository at:
> >
> > git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git
> >
> > for you to fetch changes up to 1c27b644c0fdbc61e113b8faee14baeb8df32486:
> >
> > Automate memory-barriers.txt; provide Linux-kernel memory model (2018-01-24 20:53:49 -0800)
> >
> > ----------------------------------------------------------------
> > Paul E. McKenney (1):
> > Automate memory-barriers.txt; provide Linux-kernel memory model
> >
> > tools/memory-model/Documentation/cheatsheet.txt | 30 +
> > tools/memory-model/Documentation/explanation.txt | 1840 ++++++++++++++++++++
> > tools/memory-model/Documentation/recipes.txt | 570 ++++++
> > tools/memory-model/Documentation/references.txt | 107 ++
> > tools/memory-model/MAINTAINERS | 15 +
> > tools/memory-model/README | 220 +++
> > tools/memory-model/linux-kernel.bell | 53 +
> > tools/memory-model/linux-kernel.cat | 124 ++
> > tools/memory-model/linux-kernel.cfg | 21 +
> > tools/memory-model/linux-kernel.def | 108 ++
> > .../litmus-tests/CoRR+poonceonce+Once.litmus | 19 +
> > .../litmus-tests/CoRW+poonceonce+Once.litmus | 18 +
> > .../litmus-tests/CoWR+poonceonce+Once.litmus | 18 +
> > .../litmus-tests/CoWW+poonceonce.litmus | 11 +
> > .../litmus-tests/IRIW+mbonceonces+OnceOnce.litmus | 35 +
> > .../litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 33 +
> > .../litmus-tests/ISA2+poonceonces.litmus | 28 +
> > ...cerelease+poacquirerelease+poacquireonce.litmus | 28 +
> > .../litmus-tests/LB+ctrlonceonce+mbonceonce.litmus | 23 +
> > .../LB+poacquireonce+pooncerelease.litmus | 21 +
> > .../litmus-tests/LB+poonceonces.litmus | 21 +
> > .../litmus-tests/MP+onceassign+derefonce.litmus | 25 +
> > tools/memory-model/litmus-tests/MP+polocks.litmus | 24 +
> > .../litmus-tests/MP+poonceonces.litmus | 20 +
> > .../MP+pooncerelease+poacquireonce.litmus | 20 +
> > .../memory-model/litmus-tests/MP+porevlocks.litmus | 24 +
> > .../litmus-tests/MP+wmbonceonce+rmbonceonce.litmus | 22 +
> > .../memory-model/litmus-tests/R+mbonceonces.litmus | 21 +
> > .../memory-model/litmus-tests/R+poonceonces.litmus | 19 +
> > tools/memory-model/litmus-tests/README | 125 ++
> > .../memory-model/litmus-tests/S+poonceonces.litmus | 19 +
> > .../S+wmbonceonce+poacquireonce.litmus | 20 +
> > .../litmus-tests/SB+mbonceonces.litmus | 23 +
> > .../litmus-tests/SB+poonceonces.litmus | 21 +
> > .../litmus-tests/WRC+poonceonces+Once.litmus | 27 +
> > .../WRC+pooncerelease+rmbonceonce+Once.litmus | 28 +
> > .../Z6.0+pooncelock+poonceLock+pombonce.litmus | 33 +
> > .../Z6.0+pooncelock+pooncelock+pombonce.litmus | 32 +
> > ...ooncerelease+poacquirerelease+mbonceonce.litmus | 28 +
> > tools/memory-model/lock.cat | 99 ++
> > 40 files changed, 3973 insertions(+)
> > create mode 100644 tools/memory-model/Documentation/cheatsheet.txt
> > create mode 100644 tools/memory-model/Documentation/explanation.txt
> > create mode 100644 tools/memory-model/Documentation/recipes.txt
> > create mode 100644 tools/memory-model/Documentation/references.txt
> > create mode 100644 tools/memory-model/MAINTAINERS
> > create mode 100644 tools/memory-model/README
> > create mode 100644 tools/memory-model/linux-kernel.bell
> > create mode 100644 tools/memory-model/linux-kernel.cat
> > create mode 100644 tools/memory-model/linux-kernel.cfg
> > create mode 100644 tools/memory-model/linux-kernel.def
> > create mode 100644 tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > create mode 100644 tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > create mode 100644 tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > create mode 100644 tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > create mode 100644 tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+polocks.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > create mode 100644 tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/R+mbonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/R+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/README
> > create mode 100644 tools/memory-model/litmus-tests/S+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/SB+mbonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > create mode 100644 tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > create mode 100644 tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> > create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > create mode 100644 tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> > create mode 100644 tools/memory-model/lock.cat
> >
>
> --
> #include <best/regards.h>
>
> Patrick Bellasi
>
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-09 11:29 ` Paul E. McKenney
@ 2018-02-09 12:41 ` Andrea Parri
2018-02-09 12:56 ` Paul E. McKenney
0 siblings, 1 reply; 26+ messages in thread
From: Andrea Parri @ 2018-02-09 12:41 UTC (permalink / raw)
To: Paul E. McKenney
Cc: Peter Zijlstra, Patrick Bellasi, linux-kernel, linux-arch, stern,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks
On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote:
> On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote:
> > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote:
> > > On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> > > > Hi Paul,
> > > > thanks to you and all the involved guys for this useful tool.
> > > >
> > > > I give it a try today and found that by installing herd7 by just
> > > > following the instruction in herdtools7/INSTALL.md, and precisely
> > > > installing it via:
> > > >
> > > > opam install herdtools7
> > > >
> > > > it seems to give you a tool which fails to run the basic example in
> > > > your README with this error:
> > > >
> > > > File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
> > > >
> > > > As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> > > > everything works fine.
> > > >
> > > > Maybe it's a know issue, in case just ignore me. :)
> > > >
> > > > Otherwise, maybe it can be worth to add to the README a note on which
> > > > minimum version of the herd7 tool is required.
> > > >
> > > > opma version (not working) : 7.47, Rev: exported
> > > > master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
> > >
> > > Urgh. So that's why it wouldn't work.
> > >
> > > I remember Paul saying you needed the latest version, which is why I
> > > rebuild from opam, but building top of git is a bit much.
> >
> > +1
> >
> > _Sadly_ enough, co-developers and I were aware of this issue,
> > but it was only mildly reported here (c.f.,
> >
> > https://marc.info/?l=linux-kernel&m=151638196427685&w=2 ).
> >
> > This bisects to that (crazy):
> >
> > 2d5fba7782d669c6a1cc577dbc3bf507780273bb
> > ("linux-kernel*: Make RCU identifiers match ASPLOS paper")
> >
> > From repo.: https://github.com/aparri/memory-model
> >
> > which not only did break 7.47, but also made the bell uglier
> > by mixing dashes and underscores in a very same block.
> >
> > As a solution to this issue, I can envisage a partial revert
> > of that commit (just replace those dashes); Paul, Jade, Luc:
> > any better solution?
> >
> > (Sorry for being late on IRC, glad this came out here,)
>
> Or maybe a 7.48 release?
This would work, _prior upgrade. (This's not my call of course).
I do however want to iterate, looking again at the above commit:
'rb_dep (*smp_read_barrier_depends*) ||
- 'rcu_read_lock (*rcu_read_lock*) ||
- 'rcu_read_unlock (*rcu_read_unlock*) ||
- 'sync (*synchronize_rcu*) ||
+ 'rcu-lock (*rcu_read_lock*) ||
+ 'rcu-unlock (*rcu_read_unlock*) ||
+ 'sync-rcu (*synchronize_rcu*) ||
'before_atomic (*smp_mb__before_atomic*) ||
'after_atomic (*smp_mb__after_atomic*) ||
'after_spinlock (*smp_mb__after_spinlock*)
The question arises: dash or underscore? This needs to be fixed.
Andrea
>
> Thanx, Paul
>
^ permalink raw reply [flat|nested] 26+ messages in thread
* Re: [GIT PULL tools] Linux kernel memory model
2018-02-09 12:41 ` Andrea Parri
@ 2018-02-09 12:56 ` Paul E. McKenney
0 siblings, 0 replies; 26+ messages in thread
From: Paul E. McKenney @ 2018-02-09 12:56 UTC (permalink / raw)
To: Andrea Parri
Cc: Peter Zijlstra, Patrick Bellasi, linux-kernel, linux-arch, stern,
j.alglave, luc.maranget, boqun.feng, will.deacon, npiggin,
dhowells, elena.reshetova, mhocko, akiyks
On Fri, Feb 09, 2018 at 01:41:12PM +0100, Andrea Parri wrote:
> On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote:
> > On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote:
> > > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote:
> > > > On Thu, Feb 08, 2018 at 06:41:06PM +0000, Patrick Bellasi wrote:
> > > > > Hi Paul,
> > > > > thanks to you and all the involved guys for this useful tool.
> > > > >
> > > > > I give it a try today and found that by installing herd7 by just
> > > > > following the instruction in herdtools7/INSTALL.md, and precisely
> > > > > installing it via:
> > > > >
> > > > > opam install herdtools7
> > > > >
> > > > > it seems to give you a tool which fails to run the basic example in
> > > > > your README with this error:
> > > > >
> > > > > File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros)
> > > > >
> > > > > As suggested by Will, by building instead herd7 HEAD (commit 44d69c2)
> > > > > everything works fine.
> > > > >
> > > > > Maybe it's a know issue, in case just ignore me. :)
> > > > >
> > > > > Otherwise, maybe it can be worth to add to the README a note on which
> > > > > minimum version of the herd7 tool is required.
> > > > >
> > > > > opma version (not working) : 7.47, Rev: exported
> > > > > master version (working for me) : 7.47+7(dev), Rev: 44d69c2b1b5ca0f97bd138899d31532ee5e4e084
> > > >
> > > > Urgh. So that's why it wouldn't work.
> > > >
> > > > I remember Paul saying you needed the latest version, which is why I
> > > > rebuild from opam, but building top of git is a bit much.
> > >
> > > +1
> > >
> > > _Sadly_ enough, co-developers and I were aware of this issue,
> > > but it was only mildly reported here (c.f.,
> > >
> > > https://marc.info/?l=linux-kernel&m=151638196427685&w=2 ).
> > >
> > > This bisects to that (crazy):
> > >
> > > 2d5fba7782d669c6a1cc577dbc3bf507780273bb
> > > ("linux-kernel*: Make RCU identifiers match ASPLOS paper")
> > >
> > > From repo.: https://github.com/aparri/memory-model
> > >
> > > which not only did break 7.47, but also made the bell uglier
> > > by mixing dashes and underscores in a very same block.
> > >
> > > As a solution to this issue, I can envisage a partial revert
> > > of that commit (just replace those dashes); Paul, Jade, Luc:
> > > any better solution?
> > >
> > > (Sorry for being late on IRC, glad this came out here,)
> >
> > Or maybe a 7.48 release?
>
> This would work, _prior upgrade. (This's not my call of course).
>
> I do however want to iterate, looking again at the above commit:
>
> 'rb_dep (*smp_read_barrier_depends*) ||
> - 'rcu_read_lock (*rcu_read_lock*) ||
> - 'rcu_read_unlock (*rcu_read_unlock*) ||
> - 'sync (*synchronize_rcu*) ||
> + 'rcu-lock (*rcu_read_lock*) ||
> + 'rcu-unlock (*rcu_read_unlock*) ||
> + 'sync-rcu (*synchronize_rcu*) ||
> 'before_atomic (*smp_mb__before_atomic*) ||
> 'after_atomic (*smp_mb__after_atomic*) ||
> 'after_spinlock (*smp_mb__after_spinlock*)
>
> The question arises: dash or underscore? This needs to be fixed.
The underscore in rb_dep is determined by herd, so the best shot there
is to update the model based on the de-Alpha-ication of the kernel,
thus (I believe) allowing rb_dep to be removed entirely, along with
its underscore.
As far as I know, there is nothing preventing removing underscores
from before_atomic, after_atomic, and after_spinlock, and the diff
below seems to work OK. And I did have to make a litmus test for
smp_mb__before_atomic() and smp_mb__after_atomic(). ;-)
Thoughts?
Thanx, Paul
------------------------------------------------------------------------
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b984bbda01a5..18885ad15de9 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -28,9 +28,9 @@ enum Barriers = 'wmb (*smp_wmb*) ||
'rcu-lock (*rcu_read_lock*) ||
'rcu-unlock (*rcu_read_unlock*) ||
'sync-rcu (*synchronize_rcu*) ||
- 'before_atomic (*smp_mb__before_atomic*) ||
- 'after_atomic (*smp_mb__after_atomic*) ||
- 'after_spinlock (*smp_mb__after_spinlock*)
+ 'before-atomic (*smp_mb__before_atomic*) ||
+ 'after-atomic (*smp_mb__after_atomic*) ||
+ 'after-spinlock (*smp_mb__after_spinlock*)
instructions F[Barriers]
(* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index babe2b3b0bb3..f0d27f813ec2 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -29,9 +29,9 @@ let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
let wmb = [W] ; fencerel(Wmb) ; [W]
let mb = ([M] ; fencerel(Mb) ; [M]) |
- ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
- ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
- ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
+ ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
+ ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
+ ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
let gp = po ; [Sync-rcu] ; po?
let strong-fence = mb | gp
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index a397387f77cc..f5a1eb04cb64 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -21,9 +21,9 @@ smp_mb() { __fence{mb} ; }
smp_rmb() { __fence{rmb} ; }
smp_wmb() { __fence{wmb} ; }
smp_read_barrier_depends() { __fence{rb_dep}; }
-smp_mb__before_atomic() { __fence{before_atomic} ; }
-smp_mb__after_atomic() { __fence{after_atomic} ; }
-smp_mb__after_spinlock() { __fence{after_spinlock} ; }
+smp_mb__before_atomic() { __fence{before-atomic} ; }
+smp_mb__after_atomic() { __fence{after-atomic} ; }
+smp_mb__after_spinlock() { __fence{after-spinlock} ; }
// Exchange
xchg(X,V) __xchg{mb}(X,V)
^ permalink raw reply related [flat|nested] 26+ messages in thread
end of thread, other threads:[~2018-02-09 12:56 UTC | newest]
Thread overview: 26+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-01-25 9:34 [GIT PULL tools] Linux kernel memory model Paul E. McKenney
2018-01-29 6:57 ` Ingo Molnar
2018-01-29 9:54 ` Paul E. McKenney
2018-01-31 9:00 ` Ingo Molnar
2018-01-31 10:08 ` Peter Zijlstra
2018-01-31 23:53 ` Paul E. McKenney
2018-02-01 1:17 ` Paul E. McKenney
2018-02-01 6:57 ` Ingo Molnar
2018-02-01 23:14 ` Paul E. McKenney
2018-02-02 4:46 ` Boqun Feng
2018-02-02 5:40 ` Paul E. McKenney
2018-02-03 8:48 ` Paul E. McKenney
2018-02-03 22:10 ` Alan Stern
2018-02-04 9:16 ` Paul E. McKenney
2018-02-04 10:17 ` Paul E. McKenney
2018-02-04 16:29 ` Andrea Parri
2018-02-05 5:00 ` Paul E. McKenney
2018-02-04 16:37 ` Alan Stern
2018-02-05 7:19 ` Paul E. McKenney
2018-02-08 18:41 ` Patrick Bellasi
2018-02-08 20:02 ` Peter Zijlstra
2018-02-09 9:11 ` Andrea Parri
2018-02-09 11:29 ` Paul E. McKenney
2018-02-09 12:41 ` Andrea Parri
2018-02-09 12:56 ` Paul E. McKenney
2018-02-09 11:33 ` Paul E. McKenney
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).