change system file

hc

2024-10-09 244b2c5ca8b14627e4a17755e5922221e121c771

 kernel/tools/memory-model/scripts/checklitmus.sh
..
..
@@ -1,40 +1,24 @@
1
1
 #!/bin/sh
2
+# SPDX-License-Identifier: GPL-2.0+
2
3
 #
3
-# Run a herd test and check the result against a "Result:" comment within
4
-# the litmus test.  If the verification result does not match that specified
5
-# in the litmus test, this script prints an error message prefixed with
6
-# "^^^" and exits with a non-zero status.  It also outputs verification
4
+# Run a herd7 test and invokes judgelitmus.sh to check the result against
5
+# a "Result:" comment within the litmus test.  It also outputs verification
7
6
 # results to a file whose name is that of the specified litmus test, but
8
7
 # with ".out" appended.
9
8
 #
10
9
 # Usage:
11
10
 #	checklitmus.sh file.litmus
12
11
 #
13
-# The LINUX_HERD_OPTIONS environment variable may be used to specify
14
-# arguments to herd, which default to "-conf linux-kernel.cfg".  Thus,
15
-# one would normally run this in the directory containing the memory model,
16
-# specifying the pathname of the litmus test to check.
17
-#
18
-# This program is free software; you can redistribute it and/or modify
19
-# it under the terms of the GNU General Public License as published by
20
-# the Free Software Foundation; either version 2 of the License, or
21
-# (at your option) any later version.
22
-#
23
-# This program is distributed in the hope that it will be useful,
24
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
25
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
26
-# GNU General Public License for more details.
27
-#
28
-# You should have received a copy of the GNU General Public License
29
-# along with this program; if not, you can access it online at
30
-# http://www.gnu.org/licenses/gpl-2.0.html.
12
+# Run this in the directory containing the memory model, specifying the
13
+# pathname of the litmus test to check.  The caller is expected to have
14
+# properly set up the LKMM environment variables.
31
15
 #
32
16
 # Copyright IBM Corporation, 2018
33
17
 #
34
18
 # Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
35
19
 
36
20
 litmus=$1
37
-herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg}
21
+herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
38
22
 
39
23
 if test -f "$litmus" -a -r "$litmus"
40
24
 then
..
..
@@ -43,44 +27,8 @@
43
27
 	echo ' --- ' error: \"$litmus\" is not a readable file
44
28
 	exit 255
45
29
 fi
46
-if grep -q '^ \* Result: ' $litmus
47
-then
48
-	outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
49
-else
50
-	outcome=specified
51
-fi
52
30
 
53
-echo Herd options: $herdoptions > $litmus.out
54
-/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1
55
-grep "Herd options:" $litmus.out
56
-grep '^Observation' $litmus.out
57
-if grep -q '^Observation' $litmus.out
58
-then
59
-	:
60
-else
61
-	cat $litmus.out
62
-	echo ' ^^^ Verification error'
63
-	echo ' ^^^ Verification error' >> $litmus.out 2>&1
64
-	exit 255
65
-fi
66
-if test "$outcome" = DEADLOCK
67
-then
68
-	echo grep 3 and 4
69
-	if grep '^Observation' $litmus.out | grep -q 'Never 0 0$'
70
-	then
71
-		ret=0
72
-	else
73
-		echo " ^^^ Unexpected non-$outcome verification"
74
-		echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
75
-		ret=1
76
-	fi
77
-elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe
78
-then
79
-	ret=0
80
-else
81
-	echo " ^^^ Unexpected non-$outcome verification"
82
-	echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
83
-	ret=1
84
-fi
85
-tail -2 $litmus.out | head -1
86
-exit $ret
31
+echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
32
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
33
+
34
+scripts/judgelitmus.sh $litmus