linux-kernel - [PATCH v3 tip/core/rcu 0/4] SRCU updates for 4.11

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-Id: <20170124220011.GC2269@linux.vnet.ibm.com>
Date:   Tue, 24 Jan 2017 14:00:11 -0800
From:   "Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
To:     linux-kernel@...r.kernel.org
Cc:     mingo@...nel.org, jiangshanlai@...il.com, dipankar@...ibm.com,
        akpm@...ux-foundation.org, mathieu.desnoyers@...icios.com,
        josh@...htriplett.org, tglx@...utronix.de, peterz@...radead.org,
        rostedt@...dmis.org, dhowells@...hat.com, edumazet@...gle.com,
        dvhart@...ux.intel.com, fweisbec@...il.com, oleg@...hat.com,
        bobby.prani@...il.com
Subject: [PATCH v3 tip/core/rcu 0/4] SRCU updates for 4.11

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(-)