git.maquefel.me Git - linux.git/commit

author	Paul E. McKenney <paulmck@kernel.org>
	Fri, 12 May 2023 02:12:16 +0000 (19:12 -0700)
committer	Paul E. McKenney <paulmck@kernel.org>
	Fri, 14 Jul 2023 22:10:56 +0000 (15:10 -0700)
commit	1304affd35739d83b4089a297d39ab08f1624158
tree	3c39a66766165a5983eeac72a6fc017ee7ac8aec	tree \| snapshot
parent	965167e8e6c9877390bb9574f88da21dc42f03eb	commit \| diff

rcu: Remove formal-verification tests

The CBMC-based formal-verification testing for SRCU was quite the thing
back in 2016, but the problem is that SRCU changes too quickly for the
scripting to keep up. In addition, more recently, SRCU's grace-period
ordering has been formally modeled by a group of Linux-kernel memory-model
litmus tests.

This commit therefore removes the pioneering formal-verification tests.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

40 files changed:

tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/percpu.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/preempt.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/sched.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/smp.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/workqueue.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/uapi/linux/types.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c	[deleted file]	blob \| history
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh	[deleted file]	blob \| history

ep93xx device tree rework repo: git://git.maquefel.me/linux.git

RSS Atom