Re: [GIT PULL tools] Linux kernel memory model

From: Paul E. McKenney
Date: Fri Feb 09 2018 - 06:33:59 EST

Next message: Igor Stoppa: "Re: [PATCH 3/6] struct page: add field for vm_struct"
Previous message: Tetsuo Handa: "Re: [PATCH] khungtaskd: Kick stuck processes"
In reply to: Paul E. McKenney: "Re: [GIT PULL tools] Linux kernel memory model"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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@xxxxxxxxxxxxxxxxxx
> > 2. http://lkml.kernel.org/r/20180119035855.GA29296@xxxxxxxxxxxxxxxxxx
> >
> > 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 message: Igor Stoppa: "Re: [PATCH 3/6] struct page: add field for vm_struct"
Previous message: Tetsuo Handa: "Re: [PATCH] khungtaskd: Kick stuck processes"
In reply to: Paul E. McKenney: "Re: [GIT PULL tools] Linux kernel memory model"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]