user/sven/linux.git/tools/memory-model/README, branch v5.4.149

tools/memory-model: Update the informal documentation

2019-08-09T17:28:57Z

The formal memory consistency model has added support for plain accesses (and data races). While updating the informal documentation to describe this addition to the model is highly desirable and important future work, update the informal documentation to at least acknowledge such addition. Signed-off-by: Andrea Parri Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: Akira Yokosawa Cc: Daniel Lustig Signed-off-by: Paul E. McKenney Acked-by: Alan Stern

tools/memory-model: Avoid duplicating herdtools versions

2019-03-18T17:27:52Z

Currently, herdtools version information appears no fewer than three times in the LKMM source, which is difficult to maintain. This commit therefore places the required version in one place, namely the tools/memory-model/README file. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern

tools/memory-model: Update README for addition of SRCU

2019-03-18T17:27:52Z

This commit updates the section on LKMM limitations to no longer say that SRCU is not modeled, but instead describe how LKMM's modeling of SRCU departs from the Linux-kernel implementation. TL;DR: There is no known valid use case that cares about the Linux kernel's ability to have partially overlapping SRCU read-side critical sections. Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri

tools/memory-model: Add scripts to check github litmus tests

2019-01-21T10:06:59Z

The https://github.com/paulmckrcu/litmus repository contains a large number of C-language litmus tests that include "Result:" comments predicting the verification result. This commit adds a number of scripts that run tests on these litmus tests: checkghlitmus.sh: Runs all litmus tests in the https://github.com/paulmckrcu/litmus archive that are C-language and that have "Result:" comment lines documenting expected results, comparing the actual results to those expected. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory. initlitmushist.sh Run all litmus tests having no more than the specified number of processes given a specified timeout, recording the results in .litmus.out files. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory. newlitmushist.sh For all new or updated litmus tests having no more than the specified number of processes given a specified timeout, run and record the results in .litmus.out files. checklitmushist.sh Run all litmus tests having .litmus.out files from previous initlitmushist.sh or newlitmushist.sh runs, comparing the herd output to that of the original runs. The above scripts will run litmus tests concurrently, by default with one job per available CPU. Giving any of these scripts the --help argument will cause them to print usage information. This commit also adds a number of helper scripts that are not intended to be invoked from the command line: cmplitmushist.sh: Compare the output of two different runs of the same litmus test. judgelitmus.sh: Compare the output of a litmus test to its "Result:" comment line. parseargs.sh: Parse command-line arguments. runlitmushist.sh: Run the litmus tests whose pathnames are provided one per line on standard input. While in the area, this commit also makes the existing checklitmus.sh and checkalllitmus.sh scripts use parseargs.sh in order to provide a bit of uniformity. In addition, per-litmus-test status output is directed to stdout, while end-of-test summary information is directed to stderr. Finally, the error flag standardizes on "!!!" to assist those familiar with rcutorture output. The defaults for the parseargs.sh arguments may be overridden by using environment variables: LKMM_DESTDIR for --destdir, LKMM_HERD_OPTIONS for --herdoptions, LKMM_JOBS for --jobs, LKMM_PROCS for --procs, and LKMM_TIMEOUT for --timeout. [ paulmck: History-check summary-line changes per Alan Stern feedback. ] Signed-off-by: Paul E. McKenney Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20181203230451.28921-2-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add more LKMM limitations

2018-10-02T08:28:04Z

This commit adds more detail about compiler optimizations and not-yet-modeled Linux-kernel APIs. Signed-off-by: Paul E. McKenney Reviewed-by: Andrea Parri Cc: Alexander Shishkin Cc: Arnaldo Carvalho de Melo Cc: Jiri Olsa Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Stephane Eranian Cc: Thomas Gleixner Cc: Vince Weaver Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180926182920.27644-4-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Rename litmus tests to comply to norm7

2018-07-17T07:30:36Z

norm7 produces the 'normalized' name of a litmus test, when the test can be generated from a single cycle that passes through each process exactly once. The commit renames such tests in order to comply to the naming scheme implemented by this tool. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Cc: Akira Yokosawa Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-14-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Update required version of herdtools7

2018-05-15T06:11:16Z

Code generated by klitmus7 version 7.48 doesn't compile with kernel header of 4.15 and later due to the absence of ACCESS_ONCE(). As the issue has been resolved in herdtools7 7.49, bump the required version number in README. Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney Cc: Alan Stern Cc: Andrea Parri Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Link: http://lkml.kernel.org/r/1526340837-12222-3-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Remove mention of docker/gentoo image

2018-03-10T09:22:23Z

Because the docker and gentoo images haven't been updated in quite some time, they are likely to provide more confusion than help. This commit therefore removes mention of them from the README file. Reported-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1520443660-16858-2-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add required herd7 version to README file

2018-02-21T08:58:15Z

LKMM and the herd7 tool are co-evolving, and out-of-date herd7 tools produce inaccurate results, often with no obvious error messages. This commit therefore adds the required herd7 version to the LKMM README file. Longer term, it would be good if .cat files could specify the required version in a manner allowing herd7 to produce clear diagnostics. Suggested-by: Akira Yokosawa Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Cc: Linus Torvalds Cc: Thomas Gleixner Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-9-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Clarify the origin/scope of the tool name

2018-02-21T08:58:12Z

Ingo pointed out that: "The "memory model" name is overly generic, ambiguous and somewhat misleading, as we usually mean the virtual memory layout/model when we say "memory model". GCC too uses it in that sense [...]" Make it clear that tools/memory-model/ uses the term "memory model" as shorthand for "memory consistency model" by calling out this convention in tools/memory-model/README. Stick to the original "memory model" term in sources' headers and for the subsystem name. Suggested-by: Ingo Molnar Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Acked-by: Will Deacon Acked-by: Alan Stern Cc: Linus Torvalds Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Link: http://lkml.kernel.org/r/1519169112-20593-1-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar