418b2977b3
This commit creates a formal/srcu-cbmc directory containing scripts that pull SRCU in from the source code, filter it to remove things that CBMC cannot handle, and run a series of verifications on it. This has a number of shortcomings: 1. It does not yet hook into the upper-level self-test Makefiles. 2. It tests only a single scenario, store buffering. 3. There is no gcc-based syntax-error prefiltering. Nevertheless, it does fully verify a piece of SRCU under a moderately weak memory model (PSO). Signed-off-by: Lance Roy <ldr709@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
17 lines
427 B
Makefile
17 lines
427 B
Makefile
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
|