diff options
| author | Lance Roy | 2017-01-01 01:33:50 +0100 |
|---|---|---|
| committer | Paul E. McKenney | 2017-01-25 21:54:22 +0100 |
| commit | 418b2977b34378f67c46930c72a776f94e7bf903 (patch) | |
| tree | 2f3f41dd02a80f237bda867211e4bb852c0c9a08 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore | |
| parent | srcu: Force full grace-period ordering (diff) | |
| download | kernel-qcow2-linux-418b2977b34378f67c46930c72a776f94e7bf903.tar.gz kernel-qcow2-linux-418b2977b34378f67c46930c72a776f94e7bf903.tar.xz kernel-qcow2-linux-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/tests/store_buffering/.gitignore')
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore new file mode 100644 index 000000000000..f47cb2045f13 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore @@ -0,0 +1 @@ +*.out |