All of lore.kernel.org
 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 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.