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>

1 files changed, 92 insertions, 0 deletions

diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
new file mode 100644
index 000000000000..3de5a49de49b
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
@@ -0,0 +1,92 @@
+#ifndef PERCPU_H
+#define PERCPU_H
+
+#include <stddef.h>
+#include "bug_on.h"
+#include "preempt.h"
+
+#define __percpu
+
+/* Maximum size of any percpu data. */
+#define PERCPU_OFFSET (4 * sizeof(long))
+
+/* Ignore alignment, as CBMC doesn't care about false sharing. */
+#define alloc_percpu(type) __alloc_percpu(sizeof(type), 1)
+
+static inline void *__alloc_percpu(size_t size, size_t align)
+{
+	BUG();
+	return NULL;
+}
+
+static inline void free_percpu(void *ptr)
+{
+	BUG();
+}
+
+#define per_cpu_ptr(ptr, cpu) \
+	((typeof(ptr)) ((char *) (ptr) + PERCPU_OFFSET * cpu))
+
+#define __this_cpu_inc(pcp) __this_cpu_add(pcp, 1)
+#define __this_cpu_dec(pcp) __this_cpu_sub(pcp, 1)
+#define __this_cpu_sub(pcp, n) __this_cpu_add(pcp, -(typeof(pcp)) (n))
+
+#define this_cpu_inc(pcp) this_cpu_add(pcp, 1)
+#define this_cpu_dec(pcp) this_cpu_sub(pcp, 1)
+#define this_cpu_sub(pcp, n) this_cpu_add(pcp, -(typeof(pcp)) (n))
+
+/* Make CBMC use atomics to work around bug. */
+#ifdef RUN
+#define THIS_CPU_ADD_HELPER(ptr, x) (*(ptr) += (x))
+#else
+/*
+ * Split the atomic into a read and a write so that it has the least
+ * possible ordering.
+ */
+#define THIS_CPU_ADD_HELPER(ptr, x) \
+	do { \
+		typeof(ptr) this_cpu_add_helper_ptr = (ptr); \
+		typeof(ptr) this_cpu_add_helper_x = (x); \
+		typeof(*ptr) this_cpu_add_helper_temp; \
+		__CPROVER_atomic_begin(); \
+		this_cpu_add_helper_temp = *(this_cpu_add_helper_ptr); \
+		__CPROVER_atomic_end(); \
+		this_cpu_add_helper_temp += this_cpu_add_helper_x; \
+		__CPROVER_atomic_begin(); \
+		*(this_cpu_add_helper_ptr) = this_cpu_add_helper_temp; \
+		__CPROVER_atomic_end(); \
+	} while (0)
+#endif
+
+/*
+ * For some reason CBMC needs an atomic operation even though this is percpu
+ * data.
+ */
+#define __this_cpu_add(pcp, n) \
+	do { \
+		BUG_ON(preemptible()); \
+		THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), thread_cpu_id), \
+				    (typeof(pcp)) (n)); \
+	} while (0)
+
+#define this_cpu_add(pcp, n) \
+	do { \
+		int this_cpu_add_impl_cpu = get_cpu(); \
+		THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), this_cpu_add_impl_cpu), \
+				    (typeof(pcp)) (n)); \
+		put_cpu(); \
+	} while (0)
+
+/*
+ * This will cause a compiler warning because of the cast from char[][] to
+ * type*. This will cause a compile time error if type is too big.
+ */
+#define DEFINE_PER_CPU(type, name) \
+	char name[NR_CPUS][PERCPU_OFFSET]; \
+	typedef char percpu_too_big_##name \
+		[sizeof(type) > PERCPU_OFFSET ? -1 : 1]
+
+#define for_each_possible_cpu(cpu) \
+	for ((cpu) = 0; (cpu) < NR_CPUS; ++(cpu))
+
+#endif