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: 28+ 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-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-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-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-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
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 an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.