Commit 1304affd authored by Paul E. McKenney's avatar Paul E. McKenney
Browse files

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: default avatarPaul E. McKenney <paulmck@kernel.org>
parent 965167e8

tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore

deleted100644 → 0
+0 −2
Original line number Diff line number Diff line 
# SPDX-License-Identifier: GPL-2.0-only

srcu.c

tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile

deleted100644 → 0
+0 −17
Original line number Diff line number Diff line 
# SPDX-License-Identifier: GPL-2.0

all: srcu.c store_buffering



LINUX_SOURCE = ../../../../../..



modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \

		      $(LINUX_SOURCE)/kernel/rcu/srcu.c



modified_srcu_output = include/linux/srcu.h srcu.c



include/linux/srcu.h: srcu.c



srcu.c: modify_srcu.awk Makefile $(modified_srcu_input)

	awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output)



store_buffering:

	@cd tests/store_buffering; make

tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h

deleted100644 → 0
+0 −0

Empty file deleted.

tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h

deleted100644 → 0
+0 −0

Empty file deleted.

tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h

deleted100644 → 0
+0 −0

Empty file deleted.