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 ...

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 ...
f7458a5d · Linus Torvalds · 575260e3 · a8709fa4 · f7458a5d · f7458a5d
Commit f7458a5d authored Feb 20, 2017 by Linus Torvalds
88 changed files
--- a/Documentation/RCU/Design/Data-Structures/Data-Structures.html
+++ b/Documentation/RCU/Design/Data-Structures/Data-Structures.html
@@ -4,7 +4,7 @@
        <head><title>A Tour Through TREE_RCU's Data Structures [LWN.net]</title>
        <meta HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">

-           <p>January 27, 2016</p>
+           <p>December 18, 2016</p>
           <p>This article was contributed by Paul E.&nbsp;McKenney</p>

 <h3>Introduction</h3>
@@ -31,9 +31,6 @@ to each other.
 	Accessor Functions</a>
 </ol>

-At the end we have the
-<a href="#Answers to Quick Quizzes">answers to the quick quizzes</a>.
-
 <h3><a name="Data-Structure Relationships">Data-Structure Relationships</a></h3>

 <p>RCU is for all intents and purposes a large state machine, and its

--- a/Documentation/RCU/Design/Expedited-Grace-Periods/ExpRCUFlow.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/ExpRCUFlow.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/ExpSchedFlow.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/ExpSchedFlow.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Expedited-Grace-Periods.html
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Expedited-Grace-Periods.html
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel0.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel0.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel1.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel1.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel2.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel2.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel3.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel3.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel4.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel4.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel5.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel5.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel6.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel6.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel7.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel7.svg
--- a/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel8.svg
+++ b/Documentation/RCU/Design/Expedited-Grace-Periods/Funnel8.svg
--- a/Documentation/RCU/Design/Requirements/Requirements.html
+++ b/Documentation/RCU/Design/Requirements/Requirements.html
@@ -1480,7 +1480,7 @@ speed-of-light delays if nothing else.

 <p>
 Furthermore, uncertainty about external state is inherent in many cases.
-For example, a pair of veternarians might use heartbeat to determine
+For example, a pair of veterinarians might use heartbeat to determine
 whether or not a given cat was alive.
 But how long should they wait after the last heartbeat to decide that
 the cat is in fact dead?
@@ -1489,9 +1489,9 @@ mean that a relaxed cat would be considered to cycle between death
 and life more than 100 times per minute.
 Moreover, just as with human beings, a cat's heart might stop for
 some period of time, so the exact wait period is a judgment call.
-One of our pair of veternarians might wait 30 seconds before pronouncing
+One of our pair of veterinarians might wait 30 seconds before pronouncing
 the cat dead, while the other might insist on waiting a full minute.
-The two veternarians would then disagree on the state of the cat during
+The two veterinarians would then disagree on the state of the cat during
 the final 30 seconds of the minute following the last heartbeat.

 <p>
@@ -1945,7 +1945,7 @@ guard against mishaps and misuse:
 <ol>
 <li>	It is all too easy to forget to use <tt>rcu_read_lock()</tt>
 	everywhere that it is needed, so kernels built with
-	<tt>CONFIG_PROVE_RCU=y</tt> will spat if
+	<tt>CONFIG_PROVE_RCU=y</tt> will splat if
 	<tt>rcu_dereference()</tt> is used outside of an
 	RCU read-side critical section.
 	Update-side code can use <tt>rcu_dereference_protected()</tt>,
@@ -2421,7 +2421,7 @@ However, there are some restrictions on the code placed within
 <li>	Blocking is prohibited.
 	In practice, this is not a serious restriction given that idle
 	tasks are prohibited from blocking to begin with.
-<li>	Although nesting <tt>RCU_NONIDLE()</tt> is permited, they cannot
+<li>	Although nesting <tt>RCU_NONIDLE()</tt> is permitted, they cannot
 	nest indefinitely deeply.
 	However, given that they can be nested on the order of a million
 	deep, even on 32-bit systems, this should not be a serious
@@ -2885,7 +2885,7 @@ APIs for defining and initializing <tt>srcu_struct</tt> structures.
 <h3><a name="Tasks RCU">Tasks RCU</a></h3>

 <p>
-Some forms of tracing use &ldquo;tramopolines&rdquo; to handle the
+Some forms of tracing use &ldquo;trampolines&rdquo; to handle the
 binary rewriting required to install different types of probes.
 It would be good to be able to free old trampolines, which sounds
 like a job for some form of RCU.

--- a/Documentation/RCU/trace.txt
+++ b/Documentation/RCU/trace.txt
@@ -237,7 +237,7 @@ o	"ktl" is the low-order 16 bits (in hexadecimal) of the count of

 The output of "cat rcu/rcu_preempt/rcuexp" looks as follows:

-s=21872 wd1=0 wd2=0 wd3=5 n=0 enq=0 sc=21872
+s=21872 wd1=0 wd2=0 wd3=5 enq=0 sc=21872

 These fields are as follows:

@@ -249,9 +249,6 @@ o	"wd1", "wd2", and "wd3" are the number of times that an attempt
 	completed an expedited grace period that satisfies the attempted
 	request.  "Our work is done."

-o	"n" is number of times that a concurrent CPU-hotplug operation
-	forced a fallback to a normal grace period.
-
 o	"enq" is the number of quiescent states still outstanding.

 o	"sc" is the number of times that the attempt to start a

--- a/Documentation/admin-guide/kernel-parameters.txt
+++ b/Documentation/admin-guide/kernel-parameters.txt
@@ -3269,6 +3269,13 @@
 			Lazy RCU callbacks are those which RCU can
 			prove do nothing more than free memory.

+	rcutree.rcu_kick_kthreads= [KNL]
+			Cause the grace-period kthread to get an extra
+			wake_up() if it sleeps three times longer than
+			it should at force-quiescent-state time.
+			This wake_up() will be accompanied by a
+			WARN_ONCE() splat and an ftrace_dump().
+
 	rcuperf.gp_exp= [KNL]
 			Measure performance of expedited synchronous
 			grace-period primitives.

--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
--- a/include/linux/llist.h
+++ b/include/linux/llist.h
@@ -3,28 +3,33 @@
 /*
 * Lock-less NULL terminated single linked list
 *
- * If there are multiple producers and multiple consumers, llist_add
- * can be used in producers and llist_del_all can be used in
- * consumers.  They can work simultaneously without lock.  But
- * llist_del_first can not be used here.  Because llist_del_first
- * depends on list->first->next does not changed if list->first is not
- * changed during its operation, but llist_del_first, llist_add,
- * llist_add (or llist_del_all, llist_add, llist_add) sequence in
- * another consumer may violate that.
- *
- * If there are multiple producers and one consumer, llist_add can be
- * used in producers and llist_del_all or llist_del_first can be used
- * in the consumer.
- *
- * This can be summarized as follow:
+ * Cases where locking is not needed:
+ * If there are multiple producers and multiple consumers, llist_add can be
+ * used in producers and llist_del_all can be used in consumers simultaneously
+ * without locking. Also a single consumer can use llist_del_first while
+ * multiple producers simultaneously use llist_add, without any locking.
+ *
+ * Cases where locking is needed:
+ * If we have multiple consumers with llist_del_first used in one consumer, and
+ * llist_del_first or llist_del_all used in other consumers, then a lock is
+ * needed.  This is because llist_del_first depends on list->first->next not
+ * changing, but without lock protection, there's no way to be sure about that
+ * if a preemption happens in the middle of the delete operation and on being
+ * preempted back, the list->first is the same as before causing the cmpxchg in
+ * llist_del_first to succeed. For example, while a llist_del_first operation
+ * is in progress in one consumer, then a llist_del_first, llist_add,
+ * llist_add (or llist_del_all, llist_add, llist_add) sequence in another
+ * consumer may cause violations.
+ *
+ * This can be summarized as follows:
 *
 *           |   add    | del_first |  del_all
 * add       |    -     |     -     |     -
 * del_first |          |     L     |     L
 * del_all   |          |           |     -
 *
- * Where "-" stands for no lock is needed, while "L" stands for lock
- * is needed.
+ * Where, a particular row's operation can happen concurrently with a column's
+ * operation, with "-" being no lock needed, while "L" being lock is needed.
 *
 * The list entries deleted via llist_del_all can be traversed with
 * traversing function such as llist_for_each etc.  But the list

--- a/include/linux/rcupdate.h
+++ b/include/linux/rcupdate.h
@@ -1161,5 +1161,17 @@ do { \
 		ftrace_dump(oops_dump_mode); \
 } while (0)

+/*
+ * Place this after a lock-acquisition primitive to guarantee that
+ * an UNLOCK+LOCK pair acts as a full barrier.  This guarantee applies
+ * if the UNLOCK and LOCK are executed by the same CPU or if the
+ * UNLOCK and LOCK operate on the same lock variable.
+ */
+#ifdef CONFIG_PPC
+#define smp_mb__after_unlock_lock()	smp_mb()  /* Full ordering for lock. */
+#else /* #ifdef CONFIG_PPC */
+#define smp_mb__after_unlock_lock()	do { } while (0)
+#endif /* #else #ifdef CONFIG_PPC */
+

 #endif /* __LINUX_RCUPDATE_H */
--- a/include/linux/rcutiny.h
+++ b/include/linux/rcutiny.h
@@ -27,6 +27,12 @@

 #include <linux/cache.h>

+struct rcu_dynticks;
+static inline int rcu_dynticks_snap(struct rcu_dynticks *rdtp)
+{
+	return 0;
+}
+
 static inline unsigned long get_state_synchronize_rcu(void)
 {
 	return 0;

--- a/include/linux/srcu.h
+++ b/include/linux/srcu.h
@@ -33,9 +33,9 @@
 #include <linux/rcupdate.h>
 #include <linux/workqueue.h>

-struct srcu_struct_array {
-	unsigned long c[2];
-	unsigned long seq[2];
+struct srcu_array {
+	unsigned long lock_count[2];
+	unsigned long unlock_count[2];
 };

 struct rcu_batch {
@@ -46,7 +46,7 @@ struct rcu_batch {

 struct srcu_struct {
 	unsigned long completed;
-	struct srcu_struct_array __percpu *per_cpu_ref;
+	struct srcu_array __percpu *per_cpu_ref;
 	spinlock_t queue_lock; /* protect ->batch_queue, ->running */
 	bool running;
 	/* callbacks just queued */
@@ -118,7 +118,7 @@ void process_srcu(struct work_struct *work);
 * See include/linux/percpu-defs.h for the rules on per-CPU variables.
 */
 #define __DEFINE_SRCU(name, is_static)					\
-	static DEFINE_PER_CPU(struct srcu_struct_array, name##_srcu_array);\
+	static DEFINE_PER_CPU(struct srcu_array, name##_srcu_array);\
 	is_static struct srcu_struct name = __SRCU_STRUCT_INIT(name)
 #define DEFINE_SRCU(name)		__DEFINE_SRCU(name, /* not static */)
 #define DEFINE_STATIC_SRCU(name)	__DEFINE_SRCU(name, static)

--- a/include/trace/events/rcu.h
+++ b/include/trace/events/rcu.h
@@ -385,11 +385,11 @@ TRACE_EVENT(rcu_quiescent_state_report,

 /*
 * Tracepoint for quiescent states detected by force_quiescent_state().
- * These trace events include the type of RCU, the grace-period number
- * that was blocked by the CPU, the CPU itself, and the type of quiescent
- * state, which can be "dti" for dyntick-idle mode, "ofl" for CPU offline,
- * or "kick" when kicking a CPU that has been in dyntick-idle mode for
- * too long.
+ * These trace events include the type of RCU, the grace-period number that
+ * was blocked by the CPU, the CPU itself, and the type of quiescent state,
+ * which can be "dti" for dyntick-idle mode, "ofl" for CPU offline, "kick"
+ * when kicking a CPU that has been in dyntick-idle mode for too long, or
+ * "rqc" if the CPU got a quiescent state via its rcu_qs_ctr.
 */
 TRACE_EVENT(rcu_fqs,


--- a/init/Kconfig
+++ b/init/Kconfig
--- a/kernel/locking/lockdep.c
+++ b/kernel/locking/lockdep.c
--- a/kernel/locking/locktorture.c
+++ b/kernel/locking/locktorture.c
--- a/kernel/membarrier.c
+++ b/kernel/membarrier.c
--- a/kernel/rcu/rcutorture.c
+++ b/kernel/rcu/rcutorture.c
--- a/kernel/rcu/srcu.c
+++ b/kernel/rcu/srcu.c
--- a/kernel/rcu/tiny.c
+++ b/kernel/rcu/tiny.c
--- a/kernel/rcu/tree.c
+++ b/kernel/rcu/tree.c
--- a/kernel/rcu/tree.h
+++ b/kernel/rcu/tree.h
--- a/kernel/rcu/tree_exp.h
+++ b/kernel/rcu/tree_exp.h
--- a/kernel/rcu/tree_plugin.h
+++ b/kernel/rcu/tree_plugin.h
--- a/kernel/rcu/tree_trace.c
+++ b/kernel/rcu/tree_trace.c
--- a/kernel/rcu/update.c
+++ b/kernel/rcu/update.c
--- a/lib/Kconfig.debug
+++ b/lib/Kconfig.debug
--- a/tools/testing/selftests/rcutorture/configs/rcu/CFcommon
+++ b/tools/testing/selftests/rcutorture/configs/rcu/CFcommon
 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
--- a/tools/testing/selftests/rcutorture/configs/rcu/TINY01
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TINY01
--- a/tools/testing/selftests/rcutorture/configs/rcu/TINY02
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TINY02
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE01
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE01
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE02
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE02
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE03
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE03
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE04
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE04
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE05
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE05
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE06
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE06
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE07
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE07
--- a/tools/testing/selftests/rcutorture/configs/rcu/TREE08
+++ b/tools/testing/selftests/rcutorture/configs/rcu/TREE08
--- a/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt
+++ b/tools/testing/selftests/rcutorture/doc/TREE_RCU-kconfig.txt
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore
+srcu.c
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
--- 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
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh