SRCU updates for 4.11
Get series with b4
b4 am [email protected]Versions newest first · linked by author and title
- v3 Latest4 patches 2 repliesIn review
- v23 patches 3 repliesSuperseded
- v13 patches 15 repliesSuperseded
Patches in v3 No applies recorded yet
| # | Subject and files | Size | Replies | Applied |
|---|---|---|---|---|
| 1/4 | srcu: Implement more-efficient reader countsinclude/ kernel/ kernel/ | +67 | 2 replies | |
| 2/4 | srcu: Force full grace-period orderinginclude/ kernel/ kernel/ | +20 | 0 replies | |
| 3/4 | rcutorture: Add CBMC-based formal verification for SRCUtools/ tools/ tools/ +37 more | +1582 | 0 replies | |
| 4/4 | srcu: Reduce probability of SRCU ->unlock_count[] counter overflowkernel/ | +10 | 0 replies |
Reviews trailers per patch
No Reviewed-by, Acked-by or Tested-by trailers for v3 yet.
Cover letter [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(-)