From 418b2977b34378f67c46930c72a776f94e7bf903 Mon Sep 17 00:00:00 2001 From: Lance Roy Date: Sat, 31 Dec 2016 16:33:50 -0800 Subject: rcutorture: Add CBMC-based formal verification for SRCU 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 Signed-off-by: Paul E. McKenney --- .../selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h') diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h new file mode 100644 index 000000000000..e69de29bb2d1 -- cgit v1.2.3-59-g8ed1b