From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: linux-kernel@vger.kernel.org
Cc: mingo@kernel.org, jiangshanlai@gmail.com, dipankar@in.ibm.com,
akpm@linux-foundation.org, mathieu.desnoyers@efficios.com,
josh@joshtriplett.org, tglx@linutronix.de, peterz@infradead.org,
rostedt@goodmis.org, dhowells@redhat.com, edumazet@google.com,
dvhart@linux.intel.com, fweisbec@gmail.com, oleg@redhat.com,
bobby.prani@gmail.com
Subject: [PATCH v3 tip/core/rcu 0/4] SRCU updates for 4.11
Date: Tue, 24 Jan 2017 14:00:11 -0800 [thread overview]
Message-ID: <20170124220011.GC2269@linux.vnet.ibm.com> (raw)
In-Reply-To: <20170115224128.GA20492@linux.vnet.ibm.com>
Hello!
This series provides v3 updates to SRCU:
1. This is a rewrite of the algorithm simplifying reader-count
tracking. Algorithm courtesy of Mathieu Desnoyers, implementation
courtesy of Lance Roy.
2. Force full grace-period ordering in SRCU.
3. Add CBMC-based formal verification for SRCU, courtesy of Lance Roy.
Updates since v2:
o Fix memory-barrier problems noted by Lance Roy.
o Add memory barrier to lower probability of counter overflow,
also noted by Lance Roy.
Updates since v1:
o Applied Ingo Molnar feedback.
o Fix some checkpatch issues.
Thanx, Paul
------------------------------------------------------------------------
include/linux/rcupdate.h | 12
include/linux/srcu.h | 10
kernel/rcu/rcutorture.c | 19
kernel/rcu/srcu.c | 144 +--
kernel/rcu/tree.h | 12
tools/testing/selftests/rcutorture/formal/srcu-cbmc/.gitignore | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile | 16
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/kconfig.h | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h | 155 ++++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 375 ++++++++++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h | 16
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h | 41 +
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h | 13
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c | 13
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h | 27
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c | 31
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h | 33
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h | 220 +++++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c | 11
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h | 58 +
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h | 92 ++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c | 78 ++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h | 58 +
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c | 50 +
tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h | 102 ++
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile | 11
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail | 1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c | 72 +
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh | 102 ++
34 files changed, 1679 insertions(+), 100 deletions(-)
next prev parent reply other threads:[~2017-01-24 22:00 UTC|newest]
Thread overview: 43+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-01-14 9:19 [PATCH tip/core/rcu 0/3] SRCU updates for 4.11 Paul E. McKenney
2017-01-14 9:19 ` [PATCH tip/core/rcu 1/3] srcu: More efficient reader counts Paul E. McKenney
2017-01-14 9:31 ` Ingo Molnar
2017-01-14 19:48 ` Paul E. McKenney
2017-01-14 9:20 ` [PATCH tip/core/rcu 2/3] srcu: Force full grace-period ordering Paul E. McKenney
2017-01-14 9:35 ` Ingo Molnar
2017-01-14 19:54 ` Paul E. McKenney
2017-01-14 21:41 ` Paul E. McKenney
2017-01-15 7:11 ` Ingo Molnar
2017-01-15 7:40 ` Paul E. McKenney
2017-01-15 7:57 ` Ingo Molnar
2017-01-15 9:24 ` Paul E. McKenney
2017-01-15 9:40 ` Ingo Molnar
2017-01-15 19:45 ` Paul E. McKenney
2017-01-16 6:56 ` Ingo Molnar
2017-01-23 8:12 ` Michael Ellerman
2017-01-24 2:45 ` Paul E. McKenney
2017-01-15 6:54 ` Ingo Molnar
2017-01-14 9:20 ` [PATCH tip/core/rcu 3/3] rcutorture: Add CBMC-based formal verification for SRCU Paul E. McKenney
2017-01-15 22:41 ` [PATCH tip/core/rcu v2 0/3] SRCU updates for 4.11 Paul E. McKenney
2017-01-15 22:42 ` [PATCH v2 tip/core/rcu 1/3] srcu: Implement more-efficient reader counts Paul E. McKenney
2017-01-23 20:17 ` Lance Roy
2017-01-23 20:17 ` [PATCH] SRCU: More efficient " Lance Roy
2017-01-23 20:35 ` Paul E. McKenney
2017-01-23 21:33 ` Lance Roy
2017-01-23 21:35 ` [PATCH] srcu: Implement more-efficient " Lance Roy
2017-01-24 0:42 ` Paul E. McKenney
2017-01-24 0:53 ` Lance Roy
2017-01-24 1:57 ` Paul E. McKenney
2017-01-24 3:26 ` Lance Roy
2017-01-24 17:07 ` Paul E. McKenney
2017-01-15 22:42 ` [PATCH v2 tip/core/rcu 2/3] srcu: Force full grace-period ordering Paul E. McKenney
2017-01-23 8:38 ` Lance Roy
2017-01-23 19:12 ` Paul E. McKenney
2017-01-23 20:06 ` Lance Roy
2017-01-15 22:42 ` [PATCH v2 tip/core/rcu 3/3] rcutorture: Add CBMC-based formal verification for SRCU Paul E. McKenney
2017-01-24 22:00 ` Paul E. McKenney [this message]
2017-01-24 22:00 ` [PATCH v3 tip/core/rcu 1/4] srcu: Implement more-efficient reader counts Paul E. McKenney
2017-01-25 18:17 ` Lance Roy
2017-01-25 21:03 ` Paul E. McKenney
2017-01-24 22:00 ` [PATCH v3 tip/core/rcu 2/4] srcu: Force full grace-period ordering Paul E. McKenney
2017-01-24 22:00 ` [PATCH v3 tip/core/rcu 3/4] rcutorture: Add CBMC-based formal verification for SRCU Paul E. McKenney
2017-01-24 22:00 ` [PATCH v3 tip/core/rcu 4/4] srcu: Reduce probability of SRCU ->unlock_count[] counter overflow Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20170124220011.GC2269@linux.vnet.ibm.com \
--to=paulmck@linux.vnet.ibm.com \
--cc=akpm@linux-foundation.org \
--cc=bobby.prani@gmail.com \
--cc=dhowells@redhat.com \
--cc=dipankar@in.ibm.com \
--cc=dvhart@linux.intel.com \
--cc=edumazet@google.com \
--cc=fweisbec@gmail.com \
--cc=jiangshanlai@gmail.com \
--cc=josh@joshtriplett.org \
--cc=linux-kernel@vger.kernel.org \
--cc=mathieu.desnoyers@efficios.com \
--cc=mingo@kernel.org \
--cc=oleg@redhat.com \
--cc=peterz@infradead.org \
--cc=rostedt@goodmis.org \
--cc=tglx@linutronix.de \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.