Skip to content

Commit

Permalink
tools/memory-model: Use "-unroll 0" to keep --hw runs finite
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
Paul E. McKenney committed Mar 24, 2023
1 parent 72b5f10 commit 719bef0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion tools/memory-model/scripts/runlitmus.sh
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,6 @@ then
cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
exit 253
fi
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1

exit $?

0 comments on commit 719bef0

Please sign in to comment.