Pull Linux Kernel Memory Model scripting updates from Paul McKenney:
"This improves litmus-test documentation and improves the ability to do
before/after tests on the https://github.com/paulmckrcu/litmus repo"
* tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: (32 commits)
tools/memory-model: Remove out-of-date SRCU documentation
tools/memory-model: Document LKMM test procedure
tools/memory-model: Use "grep -E" instead of "egrep"
tools/memory-model: Use "-unroll 0" to keep --hw runs finite
tools/memory-model: Make judgelitmus.sh handle scripted Result: tag
tools/memory-model: Add data-race capabilities to judgelitmus.sh
tools/memory-model: Add checktheselitmus.sh to run specified litmus tests
tools/memory-model: Repair parseargs.sh header comment
tools/memory-model: Add "--" to parseargs.sh for additional arguments
tools/memory-model: Make history-check scripts use mselect7
tools/memory-model: Make checkghlitmus.sh use mselect7
tools/memory-model: Fix scripting --jobs argument
tools/memory-model: Implement --hw support for checkghlitmus.sh
tools/memory-model: Add -v flag to jingle7 runs
tools/memory-model: Make runlitmus.sh check for jingle errors
tools/memory-model: Allow herd to deduce CPU type
tools/memory-model: Keep assembly-language litmus tests
tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw
tools/memory-model: Split runlitmus.sh out of checklitmus.sh
...
Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics")
changed the semantics of partially overlapping SRCU read-side critical
sections (among other things), making such documentation out-of-date.
The new, semantic changes are discussed in explanation.txt. Remove the
out-of-date documentation.
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit documents how to run the various scripts in order to test
a potentially pervasive change to the memory model.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The latest version of grep claims the egrep is now obsolete so the build
now contains warnings that look like:
egrep: warning: egrep is obsolescent; using grep -E
fix this up by moving the related file to use "grep -E" instead.
sed -i "s/egrep/grep -E/g" `grep egrep -rwl tools/memory-model`
Here are the steps to install the latest grep:
wget http://ftp.gnu.org/gnu/grep/grep-3.8.tar.gz
tar xf grep-3.8.tar.gz
cd grep-3.8 && ./configure && make
sudo make install
export PATH=/usr/local/bin:$PATH
Signed-off-by: Tiezhu Yang <yangtiezhu@loongson.cn>
Reviewed-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Litmus tests involving atomic operations produce LL/SC loops on a number
of architectures, and unrolling these loops can result in excessive
verification times or even stack overflows. This commit therefore uses
the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that
additional passes through an LL/SC loop should not change the verification.
Note however, that certain bugs in the mapping of the LL/SC loop to
machine instructions may go undetected. On the other hand, herd7 might
not be the best vehicle for finding such bugs in any case. (You do
stress-test your architecture-specific code, don't you?)
Suggested-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The scripts that generate the litmus tests in the "auto" directory of
the https://github.com/paulmckrcu/litmus archive place the "Result:"
tag into a single-line ocaml comment, which judgelitmus.sh currently
does not recognize. This commit therefore makes judgelitmus.sh
recognize both the multiline comment format that it currently does
and the automatically generated single-line format.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit adds functionality to judgelitmus.sh to allow it to handle
both the "DATARACE" markers in the "Result:" comments in litmus tests
and the "Flag data-race" markers in LKMM output. For C-language tests,
if either marker is present, the other must also be as well, at least for
litmus tests having a "Result:" comment. If the LKMM output indicates
a data race, then failures of the Always/Sometimes/Never portion of the
"Result:" prediction are forgiven.
The reason for forgiving "Result:" mispredictions is that data races can
result in "interesting" compiler optimizations, so that all bets are off
in the data-race case.
[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit adds a checktheselitmus.sh script that runs the litmus tests
specified on the command line. This is useful for verifying fixes to
specific litmus tests.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Currently, parseargs.sh expects to consume all the command-line arguments,
which prevents the calling script from having any of its own arguments.
This commit therefore causes parseargs.sh to stop consuming arguments
when it encounters a "--" argument, leaving any remaining arguments for
the calling script.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The history-check scripts currently use grep to ignore non-C-language
litmus tests, which is a bit fragile. This commit therefore enlists the
aid of "mselect7 -arch C", given Luc Maraget's recent modifications that
allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The checkghlitmus.sh script currently uses grep to ignore non-C-language
litmus tests, which is a bit fragile. This commit therefore enlists the
aid of "mselect7 -arch C", given Luc Maraget's recent modifications that
allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The parseargs.sh regular expression for the --jobs argument incorrectly
requires that the number of jobs be at least 10, that is, have at least
two digits. This commit therefore adjusts this regular expression to
allow single-digit numbers of jobs to be specified.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commits enables the "--hw" argument for the checkghlitmus.sh script,
causing it to convert any applicable C-language litmus tests to the
specified flavor of assembly language, to verify these assembly-language
litmus tests, and checking compatibility of the outcomes.
Note that the conversion does not yet handle locking, RCU, SRCU, plain
C-language memory accesses, or casts.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Adding the -v flag to jingle7 invocations gives much useful information
on why jingle7 didn't like a given litmus test. This commit therefore
adds this flag and saves off any such information into a .err file.
Suggested-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
It turns out that the jingle7 tool is currently a bit picky about
the litmus tests it is willing to process. This commit therefore
ensures that jingle7 failures are reported.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Currently, the scripts specify the CPU's .cat file to herd. But this is
pointless because herd will select a good and sufficient .cat file from
the assembly-language litmus test itself. This commit therefore removes
the -model argument to herd, allowing herd to figure the CPU family out
itself.
Note that the user can override herd's choice using the "--herdopts"
argument to the scripts.
Suggested-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit retains the assembly-language litmus tests generated from
the C-language litmus tests, appending the hardware tag to the original
C-language litmus test's filename. Thus, S+poonceonces.litmus.AArch64
contains the Armv8 assembly language corresponding to the C-language
S+poonceonces.litmus test.
This commit also updates the .gitignore to avoid committing these
automatically generated assembly-language litmus tests.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
When the github scripts see ".litmus.out", they assume that there must be
a corresponding C-language ".litmus" file. Won't they be disappointed
when they instead see nothing, or, worse yet, the corresponding
assembly-language litmus test? This commit therefore swaps the hardware
tag with the "litmus" to avoid this sort of disappointment.
This commit also adjusts the .gitignore file so as to avoid adding these
new ".out" files to git.
[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
In the absence of "Result:" comments, the runlitmus.sh script relies on
litmus.out files from prior LKMM runs. This can be a bit user-hostile,
so this commit makes runlitmus.sh generate any needed .litmus.out files
that don't already exist.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit prepares for adding --hw capability to github litmus-test
scripts by splitting runlitmus.sh (which simply runs the verification)
out of checklitmus.sh (which also judges the results).
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The judgelitmus.sh script currently relies solely on the "Result:"
comment in the .litmus file. This is problematic when using the --hw
argument, because it is necessary to check the hardware model against
LKMM even in the absence of "Result:" comments.
This commit therefore modifies judgelitmus.sh to check the observation
in a .litmus.out file, in case one was generated by a previous LKMM run.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit makes checklitmus.sh and checkalllitmus.sh check to see
if a hardware verification was specified (via the --hw command-line
argument, which sets the LKMM_HW_MAP_FILE environment variable).
If so, the C-language litmus test is converted to the specified type
of assembly-language litmus test and herd is run on it. Hardware is
permitted to be stronger than LKMM requires, so "Always" and "Never"
verifications of "Sometimes" C-language litmus tests are forgiven.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
The checkalllitmus.sh runs litmus tests in the litmus-tests directory,
not those in the github archive, so this commit updates the comment to
reflect this reality.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit abstracts out common function to check a given litmus test
for locking, RCU, and SRCU in order to avoid duplicating code.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
