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