summaryrefslogtreecommitdiff
path: root/tools/memory-model/scripts/runlitmus.sh
AgeCommit message (Collapse)Author
2023-03-24tools/memory-model: Use "-unroll 0" to keep --hw runs finitePaul E. McKenney
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>
2023-03-24tools/memory-model: Add -v flag to jingle7 runsPaul E. McKenney
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>
2023-03-24tools/memory-model: Make runlitmus.sh check for jingle errorsPaul E. McKenney
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>
2023-03-24tools/memory-model: Allow herd to deduce CPU typePaul E. McKenney
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>
2023-03-24tools/memory-model: Keep assembly-language litmus testsPaul E. McKenney
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>
2023-03-24tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.outPaul E. McKenney
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>
2023-03-24tools/memory-model: Make runlitmus.sh generate .litmus.out for --hwPaul E. McKenney
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>
2023-03-24tools/memory-model: Split runlitmus.sh out of checklitmus.shPaul E. McKenney
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>