linux-kernel.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH tip/core/rcu 0/3] SRCU updates for 4.11
@ 2017-01-14  9:19 Paul E. McKenney
  2017-01-14  9:19 ` [PATCH tip/core/rcu 1/3] srcu: More efficient reader counts Paul E. McKenney
                   ` (3 more replies)
  0 siblings, 4 replies; 43+ messages in thread
From: Paul E. McKenney @ 2017-01-14  9:19 UTC (permalink / raw)
  To: linux-kernel
  Cc: mingo, jiangshanlai, dipankar, akpm, mathieu.desnoyers, josh,
	tglx, peterz, rostedt, dhowells, edumazet, dvhart, fweisbec,
	oleg, bobby.prani

Hello!

This series provides 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.

							Thanx, Paul

------------------------------------------------------------------------

 include/linux/rcupdate.h                                                                  |   12 
 include/linux/srcu.h                                                                      |    4 
 kernel/rcu/rcutorture.c                                                                   |   18 
 kernel/rcu/srcu.c                                                                         |  122 +--
 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, 1661 insertions(+), 89 deletions(-)

^ permalink raw reply	[flat|nested] 43+ messages in thread

end of thread, other threads:[~2017-01-25 21:03 UTC | newest]

Thread overview: 43+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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   ` [PATCH v3 tip/core/rcu 0/4] SRCU updates for 4.11 Paul E. McKenney
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

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).