1
0
Fork 0
mirror of synced 2025-03-06 20:59:54 +01:00
Commit graph

8 commits

Author SHA1 Message Date
Paul E. McKenney
719bef0cbe tools/memory-model: Use "-unroll 0" to keep --hw runs finite
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-24 10:24:15 -07:00
Paul E. McKenney
d9313e05f0 tools/memory-model: Add -v flag to jingle7 runs
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-24 10:24:14 -07:00
Paul E. McKenney
a9504aaa9b tools/memory-model: Make runlitmus.sh check for jingle errors
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-24 10:24:14 -07:00
Paul E. McKenney
b28306a9e5 tools/memory-model: Allow herd to deduce CPU type
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-24 10:24:14 -07:00
Paul E. McKenney
2027ad41ec tools/memory-model: Keep assembly-language litmus tests
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-24 10:24:14 -07:00
Paul E. McKenney
ee542816ac tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
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-24 10:24:14 -07:00
Paul E. McKenney
dbf0b425a6 tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw
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-24 10:24:14 -07:00
Paul E. McKenney
08203824c0 tools/memory-model: Split runlitmus.sh out of checklitmus.sh
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>
2023-03-24 10:24:14 -07:00