From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Patrick Bellasi <patrick.bellasi@arm.com>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
stern@rowland.harvard.edu, parri.andrea@gmail.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, boqun.feng@gmail.com,
will.deacon@arm.com, peterz@infradead.org, npiggin@gmail.com,
dhowells@redhat.com, elena.reshetova@intel.com, mhocko@suse.com,
akiyks@gmail.com
Subject: Re: [GIT PULL tools] Linux kernel memory model
Date: Fri, 9 Feb 2018 03:33:57 -0800 [thread overview]
Message-ID: <20180209113357.GV3617@linux.vnet.ibm.com> (raw)
In-Reply-To: <20180208184106.GA17043@e110439-lin>
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
>
next prev parent reply other threads:[~2018-02-09 11:33 UTC|newest]
Thread overview: 35+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-01-25 9:34 [GIT PULL tools] Linux kernel memory model Paul E. McKenney
2018-01-25 9:34 ` 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 10:08 ` Peter Zijlstra
2018-01-31 23:53 ` Paul E. McKenney
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-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-08 20:02 ` Peter Zijlstra
2018-02-09 9:11 ` Andrea Parri
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:41 ` Andrea Parri
2018-02-09 12:56 ` Paul E. McKenney
2018-02-09 12:56 ` Paul E. McKenney
2018-02-09 11:33 ` Paul E. McKenney [this message]
2018-02-09 11:33 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20180209113357.GV3617@linux.vnet.ibm.com \
--to=paulmck@linux.vnet.ibm.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=elena.reshetova@intel.com \
--cc=j.alglave@ucl.ac.uk \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mhocko@suse.com \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=patrick.bellasi@arm.com \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will.deacon@arm.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).