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@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
