Skip to content

Commit 50c6afa

Browse files
committed
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 <[email protected]> Signed-off-by: Paul E. McKenney <[email protected]>
1 parent e92a4e8 commit 50c6afa

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tools/memory-model/scripts/runlitmus.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,6 @@ then
7575
cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
7676
exit 253
7777
fi
78-
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
78+
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
7979

8080
exit $?

0 commit comments

Comments
 (0)