tools/memory-model: Use "-unroll 0" to keep --hw runs finite
authorPaul E. McKenney <paulmck@kernel.org>
Tue, 25 Jun 2019 05:30:32 +0000 (22:30 -0700)
committerPaul E. McKenney <paulmck@kernel.org>
Wed, 2 Feb 2022 01:33:29 +0000 (17:33 -0800)
commit33a2f66a158e0d0457a6f2d7d7274a7a9d3a1a94
treee6a627944052d6b2ba26b341f667e7c3adcc1151
parent06fd59242587925fe12210df71873d6a0bf91d8f
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>
tools/memory-model/scripts/runlitmus.sh