Merge branch 'core-rcu-for-linus' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip

Pull RCU updates from Ingo Molnar:
 "The RCU changes in this cycle are:

   - Dynticks updates, consolidating open-coded counter accesses into a
     well-defined API

   - SRCU updates: Simplify algorithm, add formal verification

   - Documentation updates

   - Miscellaneous fixes

   - Torture-test updates

  Most of the diffstat comes from the relatively large documentation
  update"

* 'core-rcu-for-linus' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip: (42 commits)
  srcu: Reduce probability of SRCU ->unlock_count[] counter overflow
  rcutorture: Add CBMC-based formal verification for SRCU
  srcu: Force full grace-period ordering
  srcu: Implement more-efficient reader counts
  rcu: Adjust FQS offline checks for exact online-CPU detection
  rcu: Check cond_resched_rcu_qs() state less often to reduce GP overhead
  rcu: Abstract extended quiescent state determination
  rcu: Abstract dynticks extended quiescent state enter/exit operations
  rcu: Add lockdep checks to synchronous expedited primitives
  rcu: Eliminate unused expedited_normal counter
  llist: Clarify comments about when locking is needed
  rcu: Fix comment in rcu_organize_nocb_kthreads()
  rcu: Enable RCU tracepoints by default to aid in debugging
  rcu: Make rcu_cpu_starting() use its "cpu" argument
  rcu: Add comment headers to expedited-grace-period counter functions
  rcu: Don't wake rcuc/X kthreads on NOCB CPUs
  rcu: Re-enable TASKS_RCU for User Mode Linux
  rcu: Once again use NMI-based stack traces in stall warnings
  rcu: Remove short-term CPU kicking
  rcu: Add long-term CPU kicking
  ...

52 files changed, 1641 insertions, 8 deletions

diff --git a/tools/testing/selftests/rcutorture/configs/rcu/CFcommon b/tools/testing/selftests/rcutorture/configs/rcu/CFcommon
index f824b4c9d9d9..d2d2a86139db 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/CFcommon
+++ b/tools/testing/selftests/rcutorture/configs/rcu/CFcommon
@@ -1,5 +1,2 @@
 CONFIG_RCU_TORTURE_TEST=y
 CONFIG_PRINTK_TIME=y
-CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
-CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
-CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TINY01 b/tools/testing/selftests/rcutorture/configs/rcu/TINY01
index 0a63e073a00c..6db705e55487 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TINY01
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TINY01
@@ -7,6 +7,7 @@ CONFIG_HZ_PERIODIC=n
 CONFIG_NO_HZ_IDLE=y
 CONFIG_NO_HZ_FULL=n
 CONFIG_RCU_TRACE=n
+#CHECK#CONFIG_RCU_STALL_COMMON=n
 CONFIG_DEBUG_LOCK_ALLOC=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_PREEMPT_COUNT=n
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TINY02 b/tools/testing/selftests/rcutorture/configs/rcu/TINY02
index f1892e0371c9..a59f7686e219 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TINY02
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TINY02
@@ -8,7 +8,8 @@ CONFIG_NO_HZ_IDLE=n
 CONFIG_NO_HZ_FULL=n
 CONFIG_RCU_TRACE=y
 CONFIG_PROVE_LOCKING=y
+CONFIG_PROVE_RCU_REPEATEDLY=y
 #CHECK#CONFIG_PROVE_RCU=y
 CONFIG_DEBUG_LOCK_ALLOC=y
-CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
+CONFIG_DEBUG_OBJECTS_RCU_HEAD=y
 CONFIG_PREEMPT_COUNT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE01 b/tools/testing/selftests/rcutorture/configs/rcu/TREE01
index f572b873c620..359cb258f639 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE01
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE01
@@ -16,3 +16,6 @@ CONFIG_DEBUG_LOCK_ALLOC=n
 CONFIG_RCU_BOOST=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE02 b/tools/testing/selftests/rcutorture/configs/rcu/TREE02
index ef6a22c44dea..c1ab5926568b 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE02
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE02
@@ -20,3 +20,7 @@ CONFIG_PROVE_LOCKING=n
 CONFIG_RCU_BOOST=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
+CONFIG_DEBUG_OBJECTS_RCU_HEAD=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE03 b/tools/testing/selftests/rcutorture/configs/rcu/TREE03
index 7a17c503b382..3b93ee544e70 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE03
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE03
@@ -17,3 +17,6 @@ CONFIG_RCU_BOOST=y
 CONFIG_RCU_KTHREAD_PRIO=2
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE04 b/tools/testing/selftests/rcutorture/configs/rcu/TREE04
index 17cbe098b115..5af758e783c7 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE04
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE04
@@ -19,3 +19,7 @@ CONFIG_RCU_NOCB_CPU=n
 CONFIG_DEBUG_LOCK_ALLOC=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
+CONFIG_RCU_EQS_DEBUG=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE05 b/tools/testing/selftests/rcutorture/configs/rcu/TREE05
index 1257d3227b1e..d4cdc0d74e16 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE05
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE05
@@ -19,3 +19,6 @@ CONFIG_PROVE_LOCKING=y
 #CHECK#CONFIG_PROVE_RCU=y
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE06 b/tools/testing/selftests/rcutorture/configs/rcu/TREE06
index d3e456b74cbe..4cb02bd28f08 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE06
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE06
@@ -20,3 +20,6 @@ CONFIG_PROVE_LOCKING=y
 #CHECK#CONFIG_PROVE_RCU=y
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=y
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE07 b/tools/testing/selftests/rcutorture/configs/rcu/TREE07
index 3956b4131f72..b12a3ea1867e 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE07
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE07
@@ -19,3 +19,6 @@ CONFIG_RCU_NOCB_CPU=n
 CONFIG_DEBUG_LOCK_ALLOC=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP=y
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT=y
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT=y
diff --git a/tools/testing/selftests/rcutorture/configs/rcu/TREE08 b/tools/testing/selftests/rcutorture/configs/rcu/TREE08
index bb9b0c1a23c2..099cc63c6a3b 100644
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE08
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE08
@@ -17,8 +17,8 @@ CONFIG_RCU_FANOUT_LEAF=2
 CONFIG_RCU_NOCB_CPU=y
 CONFIG_RCU_NOCB_CPU_ALL=y
 CONFIG_DEBUG_LOCK_ALLOC=n
-CONFIG_PROVE_LOCKING=y
-#CHECK#CONFIG_PROVE_RCU=y
+CONFIG_PROVE_LOCKING=n
 CONFIG_RCU_BOOST=n
 CONFIG_DEBUG_OBJECTS_RCU_HEAD=n
 CONFIG_RCU_EXPERT=y
+CONFIG_RCU_EQS_DEBUG=y
diff --git a/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt b/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt
index 4e2b1893d40d..364801b1a230 100644
--- a/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt
+++ b/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt
@@ -14,6 +14,7 @@ CONFIG_NO_HZ_FULL_SYSIDLE -- Do one.
 CONFIG_PREEMPT -- Do half.  (First three and #8.)
 CONFIG_PROVE_LOCKING -- Do several, covering CONFIG_DEBUG_LOCK_ALLOC=y and not.
 CONFIG_PROVE_RCU -- Hardwired to CONFIG_PROVE_LOCKING.
+CONFIG_PROVE_RCU_REPEATEDLY -- Do one.
 CONFIG_RCU_BOOST -- one of PREEMPT_RCU.
 CONFIG_RCU_KTHREAD_PRIO -- set to 2 for _BOOST testing.
 CONFIG_RCU_FANOUT -- Cover hierarchy, but overlap with others.
@@ -25,7 +26,12 @@ CONFIG_RCU_NOCB_CPU_NONE -- Do one.
 CONFIG_RCU_NOCB_CPU_ZERO -- Do one.
 CONFIG_RCU_TRACE -- Do half.
 CONFIG_SMP -- Need one !SMP for PREEMPT_RCU.
-!RCU_EXPERT -- Do a few, but these have to be vanilla configurations.
+CONFIG_RCU_EXPERT=n -- Do a few, but these have to be vanilla configurations.
+CONFIG_RCU_EQS_DEBUG -- Do at least one for CONFIG_NO_HZ_FULL and not.
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP -- Do for all but a couple TREE scenarios.
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT -- Do for all but a couple TREE scenarios.
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT -- Do for all but a couple TREE scenarios.
+
 RCU-bh: Do one with PREEMPT and one with !PREEMPT.
 RCU-sched: Do one with PREEMPT but not BOOST.
 
@@ -72,7 +78,30 @@ CONFIG_RCU_TORTURE_TEST_RUNNABLE
 
         Always used in KVM testing.
 
+CONFIG_RCU_TORTURE_TEST_SLOW_PREINIT_DELAY
+CONFIG_RCU_TORTURE_TEST_SLOW_INIT_DELAY
+CONFIG_RCU_TORTURE_TEST_SLOW_CLEANUP_DELAY
+
+        Inspection suffices, ignore.
+
 CONFIG_PREEMPT_RCU
 CONFIG_TREE_RCU
+CONFIG_TINY_RCU
+
+        These are controlled by CONFIG_PREEMPT and/or CONFIG_SMP.
+
+CONFIG_SPARSE_RCU_POINTER
+
+        Makes sense only for sparse runs, not for kernel builds.
+
+CONFIG_SRCU
+CONFIG_TASKS_RCU
+
+        Selected by CONFIG_RCU_TORTURE_TEST, so cannot disable.
+
+CONFIG_RCU_TRACE
+
+        Implied by CONFIG_RCU_TRACE for Tree RCU.
+
 
-        These are controlled by CONFIG_PREEMPT.
+boot parameters ignored: TBD
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore
new file mode 100644
index 000000000000..712a3d41a325
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore
@@ -0,0 +1 @@
+srcu.c
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
new file mode 100644
index 000000000000..16b01559fa55
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
@@ -0,0 +1,16 @@
+all: srcu.c store_buffering
+
+LINUX_SOURCE = ../../../../../..
+
+modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \
+                      $(LINUX_SOURCE)/kernel/rcu/srcu.c
+
+modified_srcu_output = include/linux/srcu.h srcu.c
+
+include/linux/srcu.h: srcu.c
+
+srcu.c: modify_srcu.awk Makefile $(modified_srcu_input)
+        awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output)
+
+store_buffering:
+        @cd tests/store_buffering; make
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/delay.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/export.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/mutex.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/percpu.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/percpu.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/percpu.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/preempt.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/preempt.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/preempt.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
--- /dev/null
+++ b/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/sched.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/sched.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/sched.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/smp.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/smp.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/smp.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/workqueue.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/workqueue.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/linux/workqueue.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/uapi/linux/types.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/uapi/linux/types.h
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/empty_includes/uapi/linux/types.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
new file mode 100644
index 000000000000..1d016e66980a
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
@@ -0,0 +1 @@
+srcu.h
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h
new file mode 100644
index 000000000000..f2860dd1b407
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h
@@ -0,0 +1 @@
+#include <LINUX_SOURCE/linux/kconfig.h>
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
new file mode 100644
index 000000000000..4a3d538fef12
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
@@ -0,0 +1,155 @@
+/*
+ * This header has been modifies to remove definitions of types that
+ * are defined in standard userspace headers or are problematic for some
+ * other reason.
+ */
+
+#ifndef _LINUX_TYPES_H
+#define _LINUX_TYPES_H
+
+#define __EXPORTED_HEADERS__
+#include <uapi/linux/types.h>
+
+#ifndef __ASSEMBLY__
+
+#define DECLARE_BITMAP(name, bits) \
+        unsigned long name[BITS_TO_LONGS(bits)]
+
+typedef __u32 __kernel_dev_t;
+
+/* bsd */
+typedef unsigned char           u_char;
+typedef unsigned short          u_short;
+typedef unsigned int            u_int;
+typedef unsigned long           u_long;
+
+/* sysv */
+typedef unsigned char           unchar;
+typedef unsigned short          ushort;
+typedef unsigned int            uint;
+typedef unsigned long           ulong;
+
+#ifndef __BIT_TYPES_DEFINED__
+#define __BIT_TYPES_DEFINED__
+
+typedef         __u8            u_int8_t;
+typedef         __s8            int8_t;
+typedef         __u16           u_int16_t;
+typedef         __s16           int16_t;
+typedef         __u32           u_int32_t;
+typedef         __s32           int32_t;
+
+#endif /* !(__BIT_TYPES_DEFINED__) */
+
+typedef         __u8            uint8_t;
+typedef         __u16           uint16_t;
+typedef         __u32           uint32_t;
+
+/* this is a special 64bit data type that is 8-byte aligned */
+#define aligned_u64 __u64 __attribute__((aligned(8)))
+#define aligned_be64 __be64 __attribute__((aligned(8)))
+#define aligned_le64 __le64 __attribute__((aligned(8)))
+
+/**
+ * The type used for indexing onto a disc or disc partition.
+ *
+ * Linux always considers sectors to be 512 bytes long independently
+ * of the devices real block size.
+ *
+ * blkcnt_t is the type of the inode's block count.
+ */
+#ifdef CONFIG_LBDAF
+typedef u64 sector_t;
+#else
+typedef unsigned long sector_t;
+#endif
+
+/*
+ * The type of an index into the pagecache.
+ */
+#define pgoff_t unsigned long
+
+/*
+ * A dma_addr_t can hold any valid DMA address, i.e., any address returned
+ * by the DMA API.
+ *
+ * If the DMA API only uses 32-bit addresses, dma_addr_t need only be 32
+ * bits wide.  Bus addresses, e.g., PCI BARs, may be wider than 32 bits,
+ * but drivers do memory-mapped I/O to ioremapped kernel virtual addresses,
+ * so they don't care about the size of the actual bus addresses.
+ */
+#ifdef CONFIG_ARCH_DMA_ADDR_T_64BIT
+typedef u64 dma_addr_t;
+#else
+typedef u32 dma_addr_t;
+#endif
+
+#ifdef CONFIG_PHYS_ADDR_T_64BIT
+typedef u64 phys_addr_t;
+#else
+typedef u32 phys_addr_t;
+#endif
+
+typedef phys_addr_t resource_size_t;
+
+/*
+ * This type is the placeholder for a hardware interrupt number. It has to be
+ * big enough to enclose whatever representation is used by a given platform.
+ */
+typedef unsigned long irq_hw_number_t;
+
+typedef struct {
+        int counter;
+} atomic_t;
+
+#ifdef CONFIG_64BIT
+typedef struct {
+        long counter;
+} atomic64_t;
+#endif
+
+struct list_head {
+        struct list_head *next, *prev;
+};
+
+struct hlist_head {
+        struct hlist_node *first;
+};
+
+struct hlist_node {
+        struct hlist_node *next, **pprev;
+};
+
+/**
+ * struct callback_head - callback structure for use with RCU and task_work
+ * @next: next update requests in a list
+ * @func: actual update function to call after the grace period.
+ *
+ * The struct is aligned to size of pointer. On most architectures it happens
+ * naturally due ABI requirements, but some architectures (like CRIS) have
+ * weird ABI and we need to ask it explicitly.
+ *
+ * The alignment is required to guarantee that bits 0 and 1 of @next will be
+ * clear under normal conditions -- as long as we use call_rcu(),
+ * call_rcu_bh(), call_rcu_sched(), or call_srcu() to queue callback.
+ *
+ * This guarantee is important for few reasons:
+ *  - future call_rcu_lazy() will make use of lower bits in the pointer;
+ *  - the structure shares storage spacer in struct page with @compound_head,
+ *    which encode PageTail() in bit 0. The guarantee is needed to avoid
+ *    false-positive PageTail().
+ */
+struct callback_head {
+        struct callback_head *next;
+        void (*func)(struct callback_head *head);
+} __attribute__((aligned(sizeof(void *))));
+#define rcu_head callback_head
+
+typedef void (*rcu_callback_t)(struct rcu_head *head);
+typedef void (*call_rcu_func_t)(struct rcu_head *head, rcu_callback_t func);
+
+/* clocksource cycle base type */
+typedef u64 cycle_t;
+
+#endif /*  __ASSEMBLY__ */
+#endif /* _LINUX_TYPES_H */
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
new file mode 100755
index 000000000000..8ff89043d0a9
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
@@ -0,0 +1,375 @@
+#!/bin/awk -f
+
+# Modify SRCU for formal verification. The first argument should be srcu.h and
+# the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
+# current directory.
+
+BEGIN {
+        if (ARGC != 5) {
+                print "Usange: input.h input.c output.h output.c" > "/dev/stderr";
+                exit 1;
+        }
+        h_output = ARGV[3];
+        c_output = ARGV[4];
+        ARGC = 3;
+
+        # Tokenize using FS and not RS as FS supports regular expressions. Each
+        # record is one line of source, except that backslashed lines are
+        # combined. Comments are treated as field separators, as are quotes.
+        quote_regexp="\"([^\\\\\"]|\\\\.)*\"";
+        comment_regexp="\\/\\*([^*]|\\*+[^*/])*\\*\\/|\\/\\/.*(\n|$)";
+        FS="([ \\\\\t\n\v\f;,.=(){}+*/<>&|^-]|\\[|\\]|" comment_regexp "|" quote_regexp ")+";
+
+        inside_srcu_struct = 0;
+        inside_srcu_init_def = 0;
+        srcu_init_param_name = "";
+        in_macro = 0;
+        brace_nesting = 0;
+        paren_nesting = 0;
+
+        # Allow the manipulation of the last field separator after has been
+        # seen.
+        last_fs = "";
+        # Whether the last field separator was intended to be output.
+        last_fs_print = 0;
+
+        # rcu_batches stores the initialization for each instance of struct
+        # rcu_batch
+
+        in_comment = 0;
+
+        outputfile = "";
+}
+
+{
+        prev_outputfile = outputfile;
+        if (FILENAME ~ /\.h$/) {
+                outputfile = h_output;
+                if (FNR != NR) {
+                        print "Incorrect file order" > "/dev/stderr";
+                        exit 1;
+                }
+        }
+        else
+                outputfile = c_output;
+
+        if (prev_outputfile && outputfile != prev_outputfile) {
+                new_outputfile = outputfile;
+                outputfile = prev_outputfile;
+                update_fieldsep("", 0);
+                outputfile = new_outputfile;
+        }
+}
+
+# Combine the next line into $0.
+function combine_line() {
+        ret = getline next_line;
+        if (ret == 0) {
+                # Don't allow two consecutive getlines at the end of the file
+                if (eof_found) {
+                        print "Error: expected more input." > "/dev/stderr";
+                        exit 1;
+                } else {
+                        eof_found = 1;
+                }
+        } else if (ret == -1) {
+                print "Error reading next line of file" FILENAME > "/dev/stderr";
+                exit 1;
+        }
+        $0 = $0 "\n" next_line;
+}
+
+# Combine backslashed lines and multiline comments.
+function combine_backslashes() {
+        while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
+                combine_line();
+        }
+}
+
+function read_line() {
+        combine_line();
+        combine_backslashes();
+}
+
+# Print out field separators and update variables that depend on them. Only
+# print if p is true. Call with sep="" and p=0 to print out the last field
+# separator.
+function update_fieldsep(sep, p) {
+        # Count braces
+        sep_tmp = sep;
+        gsub(quote_regexp "|" comment_regexp, "", sep_tmp);
+        while (1)
+        {
+                if (sub("[^{}()]*\\{", "", sep_tmp)) {
+                        brace_nesting++;
+                        continue;
+                }
+                if (sub("[^{}()]*\\}", "", sep_tmp)) {
+                        brace_nesting--;
+                        if (brace_nesting < 0) {
+                                print "Unbalanced braces!" > "/dev/stderr";
+                                exit 1;
+                        }
+                        continue;
+                }
+                if (sub("[^{}()]*\\(", "", sep_tmp)) {
+                        paren_nesting++;
+                        continue;
+                }
+                if (sub("[^{}()]*\\)", "", sep_tmp)) {
+                        paren_nesting--;
+                        if (paren_nesting < 0) {
+                                print "Unbalanced parenthesis!" > "/dev/stderr";
+                                exit 1;
+                        }
+                        continue;
+                }
+
+                break;
+        }
+
+        if (last_fs_print)
+                printf("%s", last_fs) > outputfile;
+        last_fs = sep;
+        last_fs_print = p;
+}
+
+# Shifts the fields down by n positions. Calls next if there are no more. If p
+# is true then print out field separators.
+function shift_fields(n, p) {
+        do {
+                if (match($0, FS) > 0) {
+                        update_fieldsep(substr($0, RSTART, RLENGTH), p);
+                        if (RSTART + RLENGTH <= length())
+                                $0 = substr($0, RSTART + RLENGTH);
+                        else
+                                $0 = "";
+                } else {
+                        update_fieldsep("", 0);
+                        print "" > outputfile;
+                        next;
+                }
+        } while (--n > 0);
+}
+
+# Shifts and prints the first n fields.
+function print_fields(n) {
+        do {
+                update_fieldsep("", 0);
+                printf("%s", $1) > outputfile;
+                shift_fields(1, 1);
+        } while (--n > 0);
+}
+
+{
+        combine_backslashes();
+}
+
+# Print leading FS
+{
+        if (match($0, "^(" FS ")+") > 0) {
+                update_fieldsep(substr($0, RSTART, RLENGTH), 1);
+                if (RSTART + RLENGTH <= length())
+                        $0 = substr($0, RSTART + RLENGTH);
+                else
+                        $0 = "";
+        }
+}
+
+# Parse the line.
+{
+        while (NF > 0) {
+                if ($1 == "struct" && NF < 3) {
+                        read_line();
+                        continue;
+                }
+
+                if (FILENAME ~ /\.h$/ && !inside_srcu_struct &&
+                    brace_nesting == 0 && paren_nesting == 0 &&
+                    $1 == "struct" && $2 == "srcu_struct" &&
+                    $0 ~ "^struct(" FS ")+srcu_struct(" FS ")+\\{") {
+                        inside_srcu_struct = 1;
+                        print_fields(2);
+                        continue;
+                }
+                if (inside_srcu_struct && brace_nesting == 0 &&
+                    paren_nesting == 0) {
+                        inside_srcu_struct = 0;
+                        update_fieldsep("", 0);
+                        for (name in rcu_batches)
+                                print "extern struct rcu_batch " name ";" > outputfile;
+                }
+
+                if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") {
+                        # Move rcu_batches outside of the struct.
+                        rcu_batches[$3] = "";
+                        shift_fields(3, 1);
+                        sub(/;[[:space:]]*$/, "", last_fs);
+                        continue;
+                }
+
+                if (FILENAME ~ /\.h$/ && !inside_srcu_init_def &&
+                    $1 == "#define" && $2 == "__SRCU_STRUCT_INIT") {
+                        inside_srcu_init_def = 1;
+                        srcu_init_param_name = $3;
+                        in_macro = 1;
+                        print_fields(3);
+                        continue;
+                }
+                if (inside_srcu_init_def && brace_nesting == 0 &&
+                    paren_nesting == 0) {
+                        inside_srcu_init_def = 0;
+                        in_macro = 0;
+                        continue;
+                }
+
+                if (inside_srcu_init_def && brace_nesting == 1 &&
+                    paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ &&
+                    $1 ~ /^[[:alnum:]_]+$/) {
+                        name = $1;
+                        if (name in rcu_batches) {
+                                # Remove the dot.
+                                sub(/\.[[:space:]]*$/, "", last_fs);
+
+                                old_record = $0;
+                                do
+                                        shift_fields(1, 0);
+                                while (last_fs !~ /,/ || paren_nesting > 0);
+                                end_loc = length(old_record) - length($0);
+                                end_loc += index(last_fs, ",") - length(last_fs);
+
+                                last_fs = substr(last_fs, index(last_fs, ",") + 1);
+                                last_fs_print = 1;
+
+                                match(old_record, "^"name"("FS")+=");
+                                start_loc = RSTART + RLENGTH;
+
+                                len = end_loc - start_loc;
+                                initializer = substr(old_record, start_loc, len);
+                                gsub(srcu_init_param_name "\\.", "", initializer);
+                                rcu_batches[name] = initializer;
+                                continue;
+                        }
+                }
+
+                # Don't include a nonexistent file
+                if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) {
+                        update_fieldsep("", 0);
+                        next;
+                }
+
+                # Ignore most preprocessor stuff.
+                if (!in_macro && $1 ~ /#/) {
+                        break;
+                }
+
+                if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) {
+                        read_line();
+                        continue;
+                }
+                if (brace_nesting > 0 &&
+                    $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" &&
+                    $2 in rcu_batches) {
+                        # Make uses of rcu_batches global. Somewhat unreliable.
+                        shift_fields(1, 0);
+                        print_fields(1);
+                        continue;
+                }
+
+                if ($1 == "static" && NF < 3) {
+                        read_line();
+                        continue;
+                }
+                if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" ||
+                                       $2 == "void" && $3 == "srcu_flip")) {
+                        shift_fields(1, 1);
+                        print_fields(2);
+                        continue;
+                }
+
+                # Distinguish between read-side and write-side memory barriers.
+                if ($1 == "smp_mb" && NF < 2) {
+                        read_line();
+                        continue;
+                }
+                if (match($0, /^smp_mb[[:space:]();\/*]*[[:alnum:]]/)) {
+                        barrier_letter = substr($0, RLENGTH, 1);
+                        if (barrier_letter ~ /A|D/)
+                                new_barrier_name = "sync_smp_mb";
+                        else if (barrier_letter ~ /B|C/)
+                                new_barrier_name = "rs_smp_mb";
+                        else {
+                                print "Unrecognized memory barrier." > "/dev/null";
+                                exit 1;
+                        }
+
+                        shift_fields(1, 1);
+                        printf("%s", new_barrier_name) > outputfile;
+                        continue;
+                }
+
+                # Skip definition of rcu_synchronize, since it is already
+                # defined in misc.h. Only present in old versions of srcu.
+                if (brace_nesting == 0 && paren_nesting == 0 &&
+                    $1 == "struct" && $2 == "rcu_synchronize" &&
+                    $0 ~ "^struct(" FS ")+rcu_synchronize(" FS ")+\\{") {
+                        shift_fields(2, 0);
+                        while (brace_nesting) {
+                                if (NF < 2)
+                                        read_line();
+                                shift_fields(1, 0);
+                        }
+                }
+
+                # Skip definition of wakeme_after_rcu for the same reason
+                if (brace_nesting == 0 && $1 == "static" && $2 == "void" &&
+                    $3 == "wakeme_after_rcu") {
+                        while (NF < 5)
+                                read_line();
+                        shift_fields(3, 0);
+                        do {
+                                while (NF < 3)
+                                        read_line();
+                                shift_fields(1, 0);
+                        } while (paren_nesting || brace_nesting);
+                }
+
+                if ($1 ~ /^(unsigned|long)$/ && NF < 3) {
+                        read_line();
+                        continue;
+                }
+
+                # Give srcu_batches_completed the correct type for old SRCU.
+                if (brace_nesting == 0 && $1 == "long" &&
+                    $2 == "srcu_batches_completed") {
+                        update_fieldsep("", 0);
+                        printf("unsigned ") > outputfile;
+                        print_fields(2);
+                        continue;
+                }
+                if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" &&
+                    $3 == "srcu_batches_completed") {
+                        print_fields(3);
+                        continue;
+                }
+
+                # Just print out the input code by default.
+                print_fields(1);
+        }
+        update_fieldsep("", 0);
+        print > outputfile;
+        next;
+}
+
+END {
+        update_fieldsep("", 0);
+
+        if (brace_nesting != 0) {
+                print "Unbalanced braces!" > "/dev/stderr";
+                exit 1;
+        }
+
+        # Define the rcu_batches
+        for (name in rcu_batches)
+                print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output;
+}
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
new file mode 100644
index 000000000000..a64955447995
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
@@ -0,0 +1,16 @@
+#ifndef ASSUME_H
+#define ASSUME_H
+
+/* Provide an assumption macro that can be disabled for gcc. */
+#ifdef RUN
+#define assume(x) \
+        do { \
+                /* Evaluate x to suppress warnings. */ \
+                (void) (x); \
+        } while (0)
+
+#else
+#define assume(x) __CPROVER_assume(x)
+#endif
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
new file mode 100644
index 000000000000..6687acc08e6d
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
@@ -0,0 +1,41 @@
+#ifndef BARRIERS_H
+#define BARRIERS_H
+
+#define barrier() __asm__ __volatile__("" : : : "memory")
+
+#ifdef RUN
+#define smp_mb() __sync_synchronize()
+#define smp_mb__after_unlock_lock() __sync_synchronize()
+#else
+/*
+ * Copied from CBMC's implementation of __sync_synchronize(), which
+ * seems to be disabled by default.
+ */
+#define smp_mb() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
+                                 "WWcumul", "RRcumul", "RWcumul", "WRcumul")
+#define smp_mb__after_unlock_lock() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
+                                    "WWcumul", "RRcumul", "RWcumul", "WRcumul")
+#endif
+
+/*
+ * Allow memory barriers to be disabled in either the read or write side
+ * of SRCU individually.
+ */
+
+#ifndef NO_SYNC_SMP_MB
+#define sync_smp_mb() smp_mb()
+#else
+#define sync_smp_mb() do {} while (0)
+#endif
+
+#ifndef NO_READ_SIDE_SMP_MB
+#define rs_smp_mb() smp_mb()
+#else
+#define rs_smp_mb() do {} while (0)
+#endif
+
+#define ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x))
+#define READ_ONCE(x) ACCESS_ONCE(x)
+#define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val))
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
new file mode 100644
index 000000000000..2a80e91f78e7
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
@@ -0,0 +1,13 @@
+#ifndef BUG_ON_H
+#define BUG_ON_H
+
+#include <assert.h>
+
+#define BUG() assert(0)
+#define BUG_ON(x) assert(!(x))
+
+/* Does it make sense to treat warnings as errors? */
+#define WARN() BUG()
+#define WARN_ON(x) (BUG_ON(x), false)
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
new file mode 100644
index 000000000000..29eb5d2697ed
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
@@ -0,0 +1,13 @@
+#include <config.h>
+
+/* Include all source files. */
+
+#include "include_srcu.c"
+
+#include "preempt.c"
+#include "misc.c"
+
+/* Used by test.c files */
+#include <pthread.h>
+#include <stdlib.h>
+#include <linux/srcu.h>
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
new file mode 100644
index 000000000000..a60038aeea7a
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
@@ -0,0 +1,27 @@
+/* "Cheater" definitions based on restricted Kconfig choices. */
+
+#undef CONFIG_TINY_RCU
+#undef __CHECKER__
+#undef CONFIG_DEBUG_LOCK_ALLOC
+#undef CONFIG_DEBUG_OBJECTS_RCU_HEAD
+#undef CONFIG_HOTPLUG_CPU
+#undef CONFIG_MODULES
+#undef CONFIG_NO_HZ_FULL_SYSIDLE
+#undef CONFIG_PREEMPT_COUNT
+#undef CONFIG_PREEMPT_RCU
+#undef CONFIG_PROVE_RCU
+#undef CONFIG_RCU_NOCB_CPU
+#undef CONFIG_RCU_NOCB_CPU_ALL
+#undef CONFIG_RCU_STALL_COMMON
+#undef CONFIG_RCU_TRACE
+#undef CONFIG_RCU_USER_QS
+#undef CONFIG_TASKS_RCU
+#define CONFIG_TREE_RCU
+
+#define CONFIG_GENERIC_ATOMIC64
+
+#if NR_CPUS > 1
+#define CONFIG_SMP
+#else
+#undef CONFIG_SMP
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
new file mode 100644
index 000000000000..5ec582a53018
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
@@ -0,0 +1,31 @@
+#include <config.h>
+
+#include <assert.h>
+#include <errno.h>
+#include <inttypes.h>
+#include <pthread.h>
+#include <stddef.h>
+#include <string.h>
+#include <sys/types.h>
+
+#include "int_typedefs.h"
+
+#include "barriers.h"
+#include "bug_on.h"
+#include "locks.h"
+#include "misc.h"
+#include "preempt.h"
+#include "percpu.h"
+#include "workqueues.h"
+
+#ifdef USE_SIMPLE_SYNC_SRCU
+#define synchronize_srcu(sp) synchronize_srcu_original(sp)
+#endif
+
+#include <srcu.c>
+
+#ifdef USE_SIMPLE_SYNC_SRCU
+#undef synchronize_srcu
+
+#include "simple_sync_srcu.c"
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
new file mode 100644
index 000000000000..3aad63917858
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
@@ -0,0 +1,33 @@
+#ifndef INT_TYPEDEFS_H
+#define INT_TYPEDEFS_H
+
+#include <inttypes.h>
+
+typedef int8_t s8;
+typedef uint8_t u8;
+typedef int16_t s16;
+typedef uint16_t u16;
+typedef int32_t s32;
+typedef uint32_t u32;
+typedef int64_t s64;
+typedef uint64_t u64;
+
+typedef int8_t __s8;
+typedef uint8_t __u8;
+typedef int16_t __s16;
+typedef uint16_t __u16;
+typedef int32_t __s32;
+typedef uint32_t __u32;
+typedef int64_t __s64;
+typedef uint64_t __u64;
+
+#define S8_C(x) INT8_C(x)
+#define U8_C(x) UINT8_C(x)
+#define S16_C(x) INT16_C(x)
+#define U16_C(x) UINT16_C(x)
+#define S32_C(x) INT32_C(x)
+#define U32_C(x) UINT32_C(x)
+#define S64_C(x) INT64_C(x)
+#define U64_C(x) UINT64_C(x)
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
new file mode 100644
index 000000000000..356004665576
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
@@ -0,0 +1,220 @@
+#ifndef LOCKS_H
+#define LOCKS_H
+
+#include <limits.h>
+#include <pthread.h>
+#include <stdbool.h>
+
+#include "assume.h"
+#include "bug_on.h"
+#include "preempt.h"
+
+int nondet_int(void);
+
+#define __acquire(x)
+#define __acquires(x)
+#define __release(x)
+#define __releases(x)
+
+/* Only use one lock mechanism. Select which one. */
+#ifdef PTHREAD_LOCK
+struct lock_impl {
+        pthread_mutex_t mutex;
+};
+
+static inline void lock_impl_lock(struct lock_impl *lock)
+{
+        BUG_ON(pthread_mutex_lock(&lock->mutex));
+}
+
+static inline void lock_impl_unlock(struct lock_impl *lock)
+{
+        BUG_ON(pthread_mutex_unlock(&lock->mutex));
+}
+
+static inline bool lock_impl_trylock(struct lock_impl *lock)
+{
+        int err = pthread_mutex_trylock(&lock->mutex);
+
+        if (!err)
+                return true;
+        else if (err == EBUSY)
+                return false;
+        BUG();
+}
+
+static inline void lock_impl_init(struct lock_impl *lock)
+{
+        pthread_mutex_init(&lock->mutex, NULL);
+}
+
+#define LOCK_IMPL_INITIALIZER {.mutex = PTHREAD_MUTEX_INITIALIZER}
+
+#else /* !defined(PTHREAD_LOCK) */
+/* Spinlock that assumes that it always gets the lock immediately. */
+
+struct lock_impl {
+        bool locked;
+};
+
+static inline bool lock_impl_trylock(struct lock_impl *lock)
+{
+#ifdef RUN
+        /* TODO: Should this be a test and set? */
+        return __sync_bool_compare_and_swap(&lock->locked, false, true);
+#else
+        __CPROVER_atomic_begin();
+        bool old_locked = lock->locked;
+        lock->locked = true;
+        __CPROVER_atomic_end();
+
+        /* Minimal barrier to prevent accesses leaking out of lock. */
+        __CPROVER_fence("RRfence", "RWfence");
+
+        return !old_locked;
+#endif
+}
+
+static inline void lock_impl_lock(struct lock_impl *lock)
+{
+        /*
+         * CBMC doesn't support busy waiting, so just assume that the
+         * lock is available.
+         */
+        assume(lock_impl_trylock(lock));
+
+        /*
+         * If the lock was already held by this thread then the assumption
+         * is unsatisfiable (deadlock).
+         */
+}
+
+static inline void lock_impl_unlock(struct lock_impl *lock)
+{
+#ifdef RUN
+        BUG_ON(!__sync_bool_compare_and_swap(&lock->locked, true, false));
+#else
+        /* Minimal barrier to prevent accesses leaking out of lock. */
+        __CPROVER_fence("RWfence", "WWfence");
+
+        __CPROVER_atomic_begin();
+        bool old_locked = lock->locked;
+        lock->locked = false;
+        __CPROVER_atomic_end();
+
+        BUG_ON(!old_locked);
+#endif
+}
+
+static inline void lock_impl_init(struct lock_impl *lock)
+{
+        lock->locked = false;
+}
+
+#define LOCK_IMPL_INITIALIZER {.locked = false}
+
+#endif /* !defined(PTHREAD_LOCK) */
+
+/*
+ * Implement spinlocks using the lock mechanism. Wrap the lock to prevent mixing
+ * locks of different types.
+ */
+typedef struct {
+        struct lock_impl internal_lock;
+} spinlock_t;
+
+#define SPIN_LOCK_UNLOCKED {.internal_lock = LOCK_IMPL_INITIALIZER}
+#define __SPIN_LOCK_UNLOCKED(x) SPIN_LOCK_UNLOCKED
+#define DEFINE_SPINLOCK(x) spinlock_t x = SPIN_LOCK_UNLOCKED
+
+static inline void spin_lock_init(spinlock_t *lock)
+{
+        lock_impl_init(&lock->internal_lock);
+}
+
+static inline void spin_lock(spinlock_t *lock)
+{
+        /*
+         * Spin locks also need to be removed in order to eliminate all
+         * memory barriers. They are only used by the write side anyway.
+         */
+#ifndef NO_SYNC_SMP_MB
+        preempt_disable();
+        lock_impl_lock(&lock->internal_lock);
+#endif
+}
+
+static inline void spin_unlock(spinlock_t *lock)
+{
+#ifndef NO_SYNC_SMP_MB
+        lock_impl_unlock(&lock->internal_lock);
+        preempt_enable();
+#endif
+}
+
+/* Don't bother with interrupts */
+#define spin_lock_irq(lock) spin_lock(lock)
+#define spin_unlock_irq(lock) spin_unlock(lock)
+#define spin_lock_irqsave(lock, flags) spin_lock(lock)
+#define spin_unlock_irqrestore(lock, flags) spin_unlock(lock)
+
+/*
+ * This is supposed to return an int, but I think that a bool should work as
+ * well.
+ */
+static inline bool spin_trylock(spinlock_t *lock)
+{
+#ifndef NO_SYNC_SMP_MB
+        preempt_disable();
+        return lock_impl_trylock(&lock->internal_lock);
+#else
+        return true;
+#endif
+}
+
+struct completion {
+        /* Hopefuly this won't overflow. */
+        unsigned int count;
+};
+
+#define COMPLETION_INITIALIZER(x) {.count = 0}
+#define DECLARE_COMPLETION(x) struct completion x = COMPLETION_INITIALIZER(x)
+#define DECLARE_COMPLETION_ONSTACK(x) DECLARE_COMPLETION(x)
+
+static inline void init_completion(struct completion *c)
+{
+        c->count = 0;
+}
+
+static inline void wait_for_completion(struct completion *c)
+{
+        unsigned int prev_count = __sync_fetch_and_sub(&c->count, 1);
+
+        assume(prev_count);
+}
+
+static inline void complete(struct completion *c)
+{
+        unsigned int prev_count = __sync_fetch_and_add(&c->count, 1);
+
+        BUG_ON(prev_count == UINT_MAX);
+}
+
+/* This function probably isn't very useful for CBMC. */
+static inline bool try_wait_for_completion(struct completion *c)
+{
+        BUG();
+}
+
+static inline bool completion_done(struct completion *c)
+{
+        return c->count;
+}
+
+/* TODO: Implement complete_all */
+static inline void complete_all(struct completion *c)
+{
+        BUG();
+}
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
new file mode 100644
index 000000000000..ca892e3b2351
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
@@ -0,0 +1,11 @@
+#include <config.h>
+
+#include "misc.h"
+#include "bug_on.h"
+
+struct rcu_head;
+
+void wakeme_after_rcu(struct rcu_head *head)
+{
+        BUG();
+}
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h
new file mode 100644
index 000000000000..aca50030f954
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h
@@ -0,0 +1,58 @@
+#ifndef MISC_H
+#define MISC_H
+
+#include "assume.h"
+#include "int_typedefs.h"
+#include "locks.h"
+
+#include <linux/types.h>
+
+/* Probably won't need to deal with bottom halves. */
+static inline void local_bh_disable(void) {}
+static inline void local_bh_enable(void) {}
+
+#define MODULE_ALIAS(X)
+#define module_param(...)
+#define EXPORT_SYMBOL_GPL(x)
+
+#define container_of(ptr, type, member) ({                      \
+        const typeof(((type *)0)->member) *__mptr = (ptr);      \
+        (type *)((char *)__mptr - offsetof(type, member));      \
+})
+
+#ifndef USE_SIMPLE_SYNC_SRCU
+/* Abuse udelay to make sure that busy loops terminate. */
+#define udelay(x) assume(0)
+
+#else
+
+/* The simple custom synchronize_srcu is ok with try_check_zero failing. */
+#define udelay(x) do { } while (0)
+#endif
+
+#define trace_rcu_torture_read(rcutorturename, rhp, secs, c_old, c) \
+        do { } while (0)
+
+#define notrace
+
+/* Avoid including rcupdate.h */
+struct rcu_synchronize {
+        struct rcu_head head;
+        struct completion completion;
+};
+
+void wakeme_after_rcu(struct rcu_head *head);
+
+#define rcu_lock_acquire(a) do { } while (0)
+#define rcu_lock_release(a) do { } while (0)
+#define rcu_lockdep_assert(c, s) do { } while (0)
+#define RCU_LOCKDEP_WARN(c, s) do { } while (0)
+
+/* Let CBMC non-deterministically choose switch between normal and expedited. */
+bool rcu_gp_is_normal(void);
+bool rcu_gp_is_expedited(void);
+
+/* Do the same for old versions of rcu. */
+#define rcu_expedited (rcu_gp_is_expedited())
+
+#endif
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
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
new file mode 100644
index 000000000000..4f1b068e9b7a
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
@@ -0,0 +1,78 @@
+#include <config.h>
+
+#include "preempt.h"
+
+#include "assume.h"
+#include "locks.h"
+
+/* Support NR_CPUS of at most 64 */
+#define CPU_PREEMPTION_LOCKS_INIT0 LOCK_IMPL_INITIALIZER
+#define CPU_PREEMPTION_LOCKS_INIT1 \
+        CPU_PREEMPTION_LOCKS_INIT0, CPU_PREEMPTION_LOCKS_INIT0
+#define CPU_PREEMPTION_LOCKS_INIT2 \
+        CPU_PREEMPTION_LOCKS_INIT1, CPU_PREEMPTION_LOCKS_INIT1
+#define CPU_PREEMPTION_LOCKS_INIT3 \
+        CPU_PREEMPTION_LOCKS_INIT2, CPU_PREEMPTION_LOCKS_INIT2
+#define CPU_PREEMPTION_LOCKS_INIT4 \
+        CPU_PREEMPTION_LOCKS_INIT3, CPU_PREEMPTION_LOCKS_INIT3
+#define CPU_PREEMPTION_LOCKS_INIT5 \
+        CPU_PREEMPTION_LOCKS_INIT4, CPU_PREEMPTION_LOCKS_INIT4
+
+/*
+ * Simulate disabling preemption by locking a particular cpu. NR_CPUS
+ * should be the actual number of cpus, not just the maximum.
+ */
+struct lock_impl cpu_preemption_locks[NR_CPUS] = {
+        CPU_PREEMPTION_LOCKS_INIT0
+#if (NR_CPUS - 1) & 1
+        , CPU_PREEMPTION_LOCKS_INIT0
+#endif
+#if (NR_CPUS - 1) & 2
+        , CPU_PREEMPTION_LOCKS_INIT1
+#endif
+#if (NR_CPUS - 1) & 4
+        , CPU_PREEMPTION_LOCKS_INIT2
+#endif
+#if (NR_CPUS - 1) & 8
+        , CPU_PREEMPTION_LOCKS_INIT3
+#endif
+#if (NR_CPUS - 1) & 16
+        , CPU_PREEMPTION_LOCKS_INIT4
+#endif
+#if (NR_CPUS - 1) & 32
+        , CPU_PREEMPTION_LOCKS_INIT5
+#endif
+};
+
+#undef CPU_PREEMPTION_LOCKS_INIT0
+#undef CPU_PREEMPTION_LOCKS_INIT1
+#undef CPU_PREEMPTION_LOCKS_INIT2
+#undef CPU_PREEMPTION_LOCKS_INIT3
+#undef CPU_PREEMPTION_LOCKS_INIT4
+#undef CPU_PREEMPTION_LOCKS_INIT5
+
+__thread int thread_cpu_id;
+__thread int preempt_disable_count;
+
+void preempt_disable(void)
+{
+        BUG_ON(preempt_disable_count < 0 || preempt_disable_count == INT_MAX);
+
+        if (preempt_disable_count++)
+                return;
+
+        thread_cpu_id = nondet_int();
+        assume(thread_cpu_id >= 0);
+        assume(thread_cpu_id < NR_CPUS);
+        lock_impl_lock(&cpu_preemption_locks[thread_cpu_id]);
+}
+
+void preempt_enable(void)
+{
+        BUG_ON(preempt_disable_count < 1);
+
+        if (--preempt_disable_count)
+                return;
+
+        lock_impl_unlock(&cpu_preemption_locks[thread_cpu_id]);
+}
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
new file mode 100644
index 000000000000..2f95ee0e4dd5
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
@@ -0,0 +1,58 @@
+#ifndef PREEMPT_H
+#define PREEMPT_H
+
+#include <stdbool.h>
+
+#include "bug_on.h"
+
+/* This flag contains garbage if preempt_disable_count is 0. */
+extern __thread int thread_cpu_id;
+
+/* Support recursive preemption disabling. */
+extern __thread int preempt_disable_count;
+
+void preempt_disable(void);
+void preempt_enable(void);
+
+static inline void preempt_disable_notrace(void)
+{
+        preempt_disable();
+}
+
+static inline void preempt_enable_no_resched(void)
+{
+        preempt_enable();
+}
+
+static inline void preempt_enable_notrace(void)
+{
+        preempt_enable();
+}
+
+static inline int preempt_count(void)
+{
+        return preempt_disable_count;
+}
+
+static inline bool preemptible(void)
+{
+        return !preempt_count();
+}
+
+static inline int get_cpu(void)
+{
+        preempt_disable();
+        return thread_cpu_id;
+}
+
+static inline void put_cpu(void)
+{
+        preempt_enable();
+}
+
+static inline void might_sleep(void)
+{
+        BUG_ON(preempt_disable_count);
+}
+
+#endif
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c
new file mode 100644
index 000000000000..ac9cbc62b411
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c
@@ -0,0 +1,50 @@
+#include <config.h>
+
+#include <assert.h>
+#include <errno.h>
+#include <inttypes.h>
+#include <pthread.h>
+#include <stddef.h>
+#include <string.h>
+#include <sys/types.h>
+
+#include "int_typedefs.h"
+
+#include "barriers.h"
+#include "bug_on.h"
+#include "locks.h"
+#include "misc.h"
+#include "preempt.h"
+#include "percpu.h"
+#include "workqueues.h"
+
+#include <linux/srcu.h>
+
+/* Functions needed from modify_srcu.c */
+bool try_check_zero(struct srcu_struct *sp, int idx, int trycount);
+void srcu_flip(struct srcu_struct *sp);
+
+/* Simpler implementation of synchronize_srcu that ignores batching. */
+void synchronize_srcu(struct srcu_struct *sp)
+{
+        int idx;
+        /*
+         * This code assumes that try_check_zero will succeed anyway,
+         * so there is no point in multiple tries.
+         */
+        const int trycount = 1;
+
+        might_sleep();
+
+        /* Ignore the lock, as multiple writers aren't working yet anyway. */
+
+        idx = 1 ^ (sp->completed & 1);
+
+        /* For comments see srcu_advance_batches. */
+
+        assume(try_check_zero(sp, idx, trycount));
+
+        srcu_flip(sp);
+
+        assume(try_check_zero(sp, idx^1, trycount));
+}
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
new file mode 100644
index 000000000000..e58c8dfd3e90
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
@@ -0,0 +1,102 @@
+#ifndef WORKQUEUES_H
+#define WORKQUEUES_H
+
+#include <stdbool.h>
+
+#include "barriers.h"
+#include "bug_on.h"
+#include "int_typedefs.h"
+
+#include <linux/types.h>
+
+/* Stub workqueue implementation. */
+
+struct work_struct;
+typedef void (*work_func_t)(struct work_struct *work);
+void delayed_work_timer_fn(unsigned long __data);
+
+struct work_struct {
+/*      atomic_long_t data; */
+        unsigned long data;
+
+        struct list_head entry;
+        work_func_t func;
+#ifdef CONFIG_LOCKDEP
+        struct lockdep_map lockdep_map;
+#endif
+};
+
+struct timer_list {
+        struct hlist_node       entry;
+        unsigned long           expires;
+        void                    (*function)(unsigned long);
+        unsigned long           data;
+        u32                     flags;
+        int                     slack;
+};
+
+struct delayed_work {
+        struct work_struct work;
+        struct timer_list timer;
+
+        /* target workqueue and CPU ->timer uses to queue ->work */
+        struct workqueue_struct *wq;
+        int cpu;
+};
+
+
+static inline bool schedule_work(struct work_struct *work)
+{
+        BUG();
+        return true;
+}
+
+static inline bool schedule_work_on(int cpu, struct work_struct *work)
+{
+        BUG();
+        return true;
+}
+
+static inline bool queue_work(struct workqueue_struct *wq,
+                              struct work_struct *work)
+{
+        BUG();
+        return true;
+}
+
+static inline bool queue_delayed_work(struct workqueue_struct *wq,
+                                      struct delayed_work *dwork,
+                                      unsigned long delay)
+{
+        BUG();
+        return true;
+}
+
+#define INIT_WORK(w, f) \
+        do { \
+                (w)->data = 0; \
+                (w)->func = (f); \
+        } while (0)
+
+#define INIT_DELAYED_WORK(w, f) INIT_WORK(&(w)->work, (f))
+
+#define __WORK_INITIALIZER(n, f) { \
+                .data = 0, \
+                .entry = { &(n).entry, &(n).entry }, \
+                .func = f \
+        }
+
+/* Don't bother initializing timer. */
+#define __DELAYED_WORK_INITIALIZER(n, f, tflags) { \
+        .work = __WORK_INITIALIZER((n).work, (f)), \
+        }
+
+#define DECLARE_WORK(n, f) \
+        struct workqueue_struct n = __WORK_INITIALIZER
+
+#define DECLARE_DELAYED_WORK(n, f) \
+        struct delayed_work n = __DELAYED_WORK_INITIALIZER(n, f, 0)
+
+#define system_power_efficient_wq ((struct workqueue_struct *) NULL)
+
+#endif
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
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
new file mode 100644
index 000000000000..3a3aee149225
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
@@ -0,0 +1,11 @@
+CBMC_FLAGS = -I../.. -I../../src -I../../include -I../../empty_includes -32 -pointer-check -mm pso
+
+all:
+        for i in ./*.pass; do \
+                echo $$i ; \
+                CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-pass $$i > $$i.out 2>&1 ; \
+        done
+        for i in ./*.fail; do \
+                echo $$i ; \
+                CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-fail $$i > $$i.out 2>&1 ; \
+        done
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail
new file mode 100644
index 000000000000..40c8075919d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail
@@ -0,0 +1 @@
+test_cbmc_options="-DASSERT_END"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail
new file mode 100644
index 000000000000..ada5baf0b60d
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail
@@ -0,0 +1 @@
+test_cbmc_options="-DFORCE_FAILURE"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail
new file mode 100644
index 000000000000..8fe00c8db466
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail
@@ -0,0 +1 @@
+test_cbmc_options="-DFORCE_FAILURE_2"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail
new file mode 100644
index 000000000000..612ed6772844
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail
@@ -0,0 +1 @@
+test_cbmc_options="-DFORCE_FAILURE_3"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass
new file mode 100644
index 000000000000..e69de29bb2d1
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c
new file mode 100644
index 000000000000..470b1105a112
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c
@@ -0,0 +1,72 @@
+#include <src/combined_source.c>
+
+int x;
+int y;
+
+int __unbuffered_tpr_x;
+int __unbuffered_tpr_y;
+
+DEFINE_SRCU(ss);
+
+void rcu_reader(void)
+{
+        int idx;
+
+#ifndef FORCE_FAILURE_3
+        idx = srcu_read_lock(&ss);
+#endif
+        might_sleep();
+
+        __unbuffered_tpr_y = READ_ONCE(y);
+#ifdef FORCE_FAILURE
+        srcu_read_unlock(&ss, idx);
+        idx = srcu_read_lock(&ss);
+#endif
+        WRITE_ONCE(x, 1);
+
+#ifndef FORCE_FAILURE_3
+        srcu_read_unlock(&ss, idx);
+#endif
+        might_sleep();
+}
+
+void *thread_update(void *arg)
+{
+        WRITE_ONCE(y, 1);
+#ifndef FORCE_FAILURE_2
+        synchronize_srcu(&ss);
+#endif
+        might_sleep();
+        __unbuffered_tpr_x = READ_ONCE(x);
+
+        return NULL;
+}
+
+void *thread_process_reader(void *arg)
+{
+        rcu_reader();
+
+        return NULL;
+}
+
+int main(int argc, char *argv[])
+{
+        pthread_t tu;
+        pthread_t tpr;
+
+        if (pthread_create(&tu, NULL, thread_update, NULL))
+                abort();
+        if (pthread_create(&tpr, NULL, thread_process_reader, NULL))
+                abort();
+        if (pthread_join(tu, NULL))
+                abort();
+        if (pthread_join(tpr, NULL))
+                abort();
+        assert(__unbuffered_tpr_y != 0 || __unbuffered_tpr_x != 0);
+
+#ifdef ASSERT_END
+        assert(0);
+#endif
+
+        return 0;
+}
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
new file mode 100755
index 000000000000..d1545972a0fa
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
@@ -0,0 +1,102 @@
+#!/bin/sh
+
+# This script expects a mode (either --should-pass or --should-fail) followed by
+# an input file. The script uses the following environment variables. The test C
+# source file is expected to be named test.c in the directory containing the
+# input file.
+#
+# CBMC: The command to run CBMC. Default: cbmc
+# CBMC_FLAGS: Additional flags to pass to CBMC
+# NR_CPUS: Number of cpus to run tests with. Default specified by the test
+# SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple.
+#                 kernel: Version included in the linux kernel source.
+#                 simple: Use try_check_zero directly.
+#
+# The input file is a script that is sourced by this file. It can define any of
+# the following variables to configure the test.
+#
+# test_cbmc_options: Extra options to pass to CBMC.
+# min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail.
+#                The test is expected to pass if it is run with fewer. (Only
+#                useful for .fail files)
+# default_cpus: Quantity of CPUs to use for the test, if not specified on the
+#               command line. Default: Larger of 2 and MIN_CPUS_FAIL.
+
+set -e
+
+if test "$#" -ne 2; then
+        echo "Expected one option followed by an input file" 1>&2
+        exit 99
+fi
+
+if test "x$1" = "x--should-pass"; then
+        should_pass="yes"
+elif test "x$1" = "x--should-fail"; then
+        should_pass="no"
+else
+        echo "Unrecognized argument '$1'" 1>&2
+
+        # Exit code 99 indicates a hard error.
+        exit 99
+fi
+
+CBMC=${CBMC:-cbmc}
+
+SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple}
+
+case ${SYNC_SRCU_MODE} in
+kernel) sync_srcu_mode_flags="" ;;
+simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;;
+
+*)
+        echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2
+        exit 99
+        ;;
+esac
+
+min_cpus_fail=1
+
+c_file=`dirname "$2"`/test.c
+
+# Source the input file.
+. $2
+
+if test ${min_cpus_fail} -gt 2; then
+        default_default_cpus=${min_cpus_fail}
+else
+        default_default_cpus=2
+fi
+default_cpus=${default_cpus:-${default_default_cpus}}
+cpus=${NR_CPUS:-${default_cpus}}
+
+# Check if there are two few cpus to make the test fail.
+if test $cpus -lt ${min_cpus_fail:-0}; then
+        should_pass="yes"
+fi
+
+cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}"
+
+echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}"
+if ${CBMC} ${cbmc_opts} "${c_file}"; then
+        # Verification successful. Make sure that it was supposed to verify.
+        test "x${should_pass}" = xyes
+else
+        cbmc_exit_status=$?
+
+        # An exit status of 10 indicates a failed verification.
+        # (see cbmc_parse_optionst::do_bmc in the CBMC source code)
+        if test ${cbmc_exit_status} -eq 10 && test "x${should_pass}" = xno; then
+                :
+        else
+                echo "CBMC returned ${cbmc_exit_status} exit status" 1>&2
+
+                # Parse errors have exit status 6. Any other type of error
+                # should be considered a hard error.
+                if test ${cbmc_exit_status} -ne 6 && \
+                   test ${cbmc_exit_status} -ne 10; then
+                        exit 99
+                else
+                        exit 1
+                fi
+        fi
+fi