projects / linux.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d85b62f) | patch
rcutorture: Add CBMC-based formal verification for SRCU
authorLance Roy <ldr709@gmail.com>
Sun, 1 Jan 2017 00:33:50 +0000 (16:33 -0800)
committerPaul E. McKenney <paulmck@linux.vnet.ibm.com>
Wed, 25 Jan 2017 20:54:22 +0000 (12:54 -0800)
commit418b2977b34378f67c46930c72a776f94e7bf903
tree2f3f41dd02a80f237bda867211e4bb852c0c9a08tree | snapshot
parentd85b62f18d543c663cbdd6061054efeb9e66cee7commit | diff
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>
40 files changed:
tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/percpu.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/preempt.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/rcupdate.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/sched.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/smp.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/workqueue.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/uapi/linux/types.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk [new file with mode: 0755] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c [new file with mode: 0644] blob
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh [new file with mode: 0755] blob
ep93xx device tree rework repo: git://git.maquefel.me/linux.git