tools/memory-model: Add scripts to check github litmus tests (b02eb5b0) · Commits · 戴 / test

tools/memory-model/.gitignore

0 → 100644

+1 −0

Original line number	Diff line number	Diff line
		litmus

tools/memory-model/README

+2 −0

Original line number	Diff line number	Diff line
		@@ -156,6 +156,8 @@ lock.cat
		README
		This file.

		scripts Various scripts, see scripts/README.


		===========
		LIMITATIONS

tools/memory-model/scripts/README

0 → 100644

+70 −0

Original line number	Diff line number	Diff line
		============
		LKMM SCRIPTS
		============


		These scripts are run from the tools/memory-model directory.

		checkalllitmus.sh

		Run all litmus tests in the litmus-tests directory, checking
		the results against the expected results recorded in the
		"Result:" comment lines.

		checkghlitmus.sh

		Run all litmus tests in the https://github.com/paulmckrcu/litmus
		archive that are C-language and that have "Result:" comment lines
		documenting expected results, comparing the actual results to
		those expected.

		checklitmushist.sh

		Run all litmus tests having .litmus.out files from previous
		initlitmushist.sh or newlitmushist.sh runs, comparing the
		herd output to that of the original runs.

		checklitmus.sh

		Check a single litmus test against its "Result:" expected result.

		cmplitmushist.sh

		Compare output from two different runs of the same litmus tests,
		with the absolute pathnames of the tests to run provided one
		name per line on standard input. Not normally run manually,
		provided instead for use by other scripts.

		initlitmushist.sh

		Run all litmus tests having no more than the specified number
		of processes given a specified timeout, recording the results
		in .litmus.out files.

		judgelitmus.sh

		Given a .litmus file and its .litmus.out herd output, check the
		.litmus.out file against the .litmus file's "Result:" comment to
		judge whether the test ran correctly. Not normally run manually,
		provided instead for use by other scripts.

		newlitmushist.sh

		For all new or updated litmus tests having no more than the
		specified number of processes given a specified timeout, run
		and record the results in .litmus.out files.

		parseargs.sh

		Parse command-line arguments. Not normally run manually,
		provided instead for use by other scripts.

		runlitmushist.sh

		Run the litmus tests whose absolute pathnames are provided one
		name per line on standard input. Not normally run manually,
		provided instead for use by other scripts.

		README

		This file

tools/memory-model/scripts/checkalllitmus.sh

+23 −30

Original line number	Diff line number	Diff line
		#!/bin/sh
		# SPDX-License-Identifier: GPL-2.0+
		#
		# Run herd tests on all .litmus files in the specified directory (which
		# defaults to litmus-tests) and check each file's result against a "Result:"
		# comment within that litmus test. If the verification result does not
		# match that specified in the litmus test, this script prints an error
		# message prefixed with "^^^". It also outputs verification results to
		# a file whose name is that of the specified litmus test, but with ".out"
		# appended.
		# Run herd tests on all .litmus files in the litmus-tests directory
		# and check each file's result against a "Result:" comment within that
		# litmus test. If the verification result does not match that specified
		# in the litmus test, this script prints an error message prefixed with
		# "^^^". It also outputs verification results to a file whose name is
		# that of the specified litmus test, but with ".out" appended.
		#
		# Usage:
		# checkalllitmus.sh [ directory ]
		# checkalllitmus.sh
		#
		# The LINUX_HERD_OPTIONS environment variable may be used to specify
		# arguments to herd, whose default is defined by the checklitmus.sh script.
		# Thus, one would normally run this in the directory containing the memory
		# model, specifying the pathname of the litmus test to check.
		# Run this in the directory containing the memory model.
		#
		# This script makes no attempt to run the litmus tests concurrently.
		#
		# This program is free software; you can redistribute it and/or modify
		# it under the terms of the GNU General Public License as published by
		# the Free Software Foundation; either version 2 of the License, or
		# (at your option) any later version.
		#
		# This program is distributed in the hope that it will be useful,
		# but WITHOUT ANY WARRANTY; without even the implied warranty of
		# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
		# GNU General Public License for more details.
		#
		# You should have received a copy of the GNU General Public License
		# along with this program; if not, you can access it online at
		# http://www.gnu.org/licenses/gpl-2.0.html.
		#
		# Copyright IBM Corporation, 2018
		#
		# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

		litmusdir=${1-litmus-tests}
		. scripts/parseargs.sh

		litmusdir=litmus-tests
		if test -d "$litmusdir" -a -r "$litmusdir" -a -x "$litmusdir"
		then
		:
		@@ -45,6 +30,14 @@ else
		exit 255
		fi

		# Create any new directories that have appeared in the github litmus
		# repo since the last run.
		if test "$LKMM_DESTDIR" != "."
		then
		find $litmusdir -type d -print \|
		( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' \| sh )
		fi

		# Find the checklitmus script. If it is not where we expect it, then
		# assume that the caller has the PATH environment variable set
		# appropriately.
		@@ -57,7 +50,7 @@ fi

		# Run the script on all the litmus tests in the specified directory
		ret=0
		for i in litmus-tests/*.litmus
		for i in $litmusdir/*.litmus
		do
		if ! $clscript $i
		then
		@@ -66,8 +59,8 @@ do
		done
		if test "$ret" -ne 0
		then
		echo " ^^^ VERIFICATION MISMATCHES"
		echo " ^^^ VERIFICATION MISMATCHES" 1>&2
		else
		echo All litmus tests verified as was expected.
		echo All litmus tests verified as was expected. 1>&2
		fi
		exit $ret

tools/memory-model/scripts/checkghlitmus.sh

0 → 100644

+65 −0

Original line number	Diff line number	Diff line
		#!/bin/sh
		# SPDX-License-Identifier: GPL-2.0+
		#
		# Runs the C-language litmus tests having a maximum number of processes
		# to run, defaults to 6.
		#
		# sh checkghlitmus.sh
		#
		# Run from the Linux kernel tools/memory-model directory. See the
		# parseargs.sh scripts for arguments.

		. scripts/parseargs.sh

		T=/tmp/checkghlitmus.sh.$$
		trap 'rm -rf $T' 0
		mkdir $T

		# Clone the repository if it is not already present.
		if test -d litmus
		then
		:
		else
		git clone https://github.com/paulmckrcu/litmus
		( cd litmus; git checkout origin/master )
		fi

		# Create any new directories that have appeared in the github litmus
		# repo since the last run.
		if test "$LKMM_DESTDIR" != "."
		then
		find litmus -type d -print \|
		( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' \| sh )
		fi

		# Create a list of the C-language litmus tests previously run.
		( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) \|
		sed -e 's/\.out$//' \|
		xargs -r egrep -l '^ \* Result: (Never\|Sometimes\|Always\|DEADLOCK)' \|
		xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already

		# Create a list of C-language litmus tests with "Result:" commands and
		# no more than the specified number of processes.
		find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
		xargs < $T/list-C -r egrep -l '^ \* Result: (Never\|Sometimes\|Always\|DEADLOCK)' > $T/list-C-result
		xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short

		# Form list of tests without corresponding .litmus.out files
		sort $T/list-C-already $T/list-C-result-short \| uniq -u > $T/list-C-needed

		# Run any needed tests.
		if scripts/runlitmushist.sh < $T/list-C-needed > $T/run.stdout 2> $T/run.stderr
		then
		errs=
		else
		errs=1
		fi

		sed < $T/list-C-result-short -e 's,^,scripts/judgelitmus.sh ,' \|
		sh > $T/judge.stdout 2> $T/judge.stderr

		if test -n "$errs"
		then
		cat $T/run.stderr 1>&2
		fi
		grep '!!!' $T/judge.stdout

Admin message