From: Patrick Bellasi <patrick.bellasi@arm.com>
To: "Paul E. McKenney" <paulmck@linux.vnet.ibm.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: Thu, 8 Feb 2018 18:41:06 +0000 [thread overview]
Message-ID: <20180208184106.GA17043@e110439-lin> (raw)
In-Reply-To: <20180125093440.GA875@linux.vnet.ibm.com>
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
next prev parent reply other threads:[~2018-02-08 18:41 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 [this message]
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
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=20180208184106.GA17043@e110439-lin \
--to=patrick.bellasi@arm.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=paulmck@linux.vnet.ibm.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).