diff options
author | Lance Roy <ldr709@gmail.com> | 2016-12-31 16:33:50 -0800 |
---|---|---|
committer | Paul E. McKenney <paulmck@linux.vnet.ibm.com> | 2017-01-25 12:54:22 -0800 |
commit | 418b2977b34378f67c46930c72a776f94e7bf903 (patch) | |
tree | 2f3f41dd02a80f237bda867211e4bb852c0c9a08 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h | |
parent | srcu: Force full grace-period ordering (diff) | |
download | linux-dev-418b2977b34378f67c46930c72a776f94e7bf903.tar.xz linux-dev-418b2977b34378f67c46930c72a776f94e7bf903.zip |
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 <ldr709@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h | 0 |
1 files changed, 0 insertions, 0 deletions
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 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h |