diff options
author | Linus Torvalds <torvalds@linux-foundation.org> | 2017-02-20 11:21:17 -0800 |
---|---|---|
committer | Linus Torvalds <torvalds@linux-foundation.org> | 2017-02-20 11:21:17 -0800 |
commit | f7458a5d631df2ecdbfe4a606053aba19913cc41 (patch) | |
tree | 26df2860fe3a750ed3b0359178d2b4c4fe8798d2 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering | |
parent | 575260e3f8f8ac72dc0c41a4a20190d1a5f2b887 (diff) | |
parent | a8709fa4a06d4af5f86e3660839531cbe0f2a19b (diff) | |
download | linux-f7458a5d631df2ecdbfe4a606053aba19913cc41.tar.bz2 |
Merge branch 'core-rcu-for-linus' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip
Pull RCU updates from Ingo Molnar:
"The RCU changes in this cycle are:
- Dynticks updates, consolidating open-coded counter accesses into a
well-defined API
- SRCU updates: Simplify algorithm, add formal verification
- Documentation updates
- Miscellaneous fixes
- Torture-test updates
Most of the diffstat comes from the relatively large documentation
update"
* 'core-rcu-for-linus' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip: (42 commits)
srcu: Reduce probability of SRCU ->unlock_count[] counter overflow
rcutorture: Add CBMC-based formal verification for SRCU
srcu: Force full grace-period ordering
srcu: Implement more-efficient reader counts
rcu: Adjust FQS offline checks for exact online-CPU detection
rcu: Check cond_resched_rcu_qs() state less often to reduce GP overhead
rcu: Abstract extended quiescent state determination
rcu: Abstract dynticks extended quiescent state enter/exit operations
rcu: Add lockdep checks to synchronous expedited primitives
rcu: Eliminate unused expedited_normal counter
llist: Clarify comments about when locking is needed
rcu: Fix comment in rcu_organize_nocb_kthreads()
rcu: Enable RCU tracepoints by default to aid in debugging
rcu: Make rcu_cpu_starting() use its "cpu" argument
rcu: Add comment headers to expedited-grace-period counter functions
rcu: Don't wake rcuc/X kthreads on NOCB CPUs
rcu: Re-enable TASKS_RCU for User Mode Linux
rcu: Once again use NMI-based stack traces in stall warnings
rcu: Remove short-term CPU kicking
rcu: Add long-term CPU kicking
...
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering')
8 files changed, 88 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore new file mode 100644 index 000000000000..f47cb2045f13 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile new file mode 100644 index 000000000000..3a3aee149225 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile @@ -0,0 +1,11 @@ +CBMC_FLAGS = -I../.. -I../../src -I../../include -I../../empty_includes -32 -pointer-check -mm pso + +all: + for i in ./*.pass; do \ + echo $$i ; \ + CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-pass $$i > $$i.out 2>&1 ; \ + done + for i in ./*.fail; do \ + echo $$i ; \ + CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-fail $$i > $$i.out 2>&1 ; \ + done diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail new file mode 100644 index 000000000000..40c8075919d1 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/assert_end.fail @@ -0,0 +1 @@ +test_cbmc_options="-DASSERT_END" diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail new file mode 100644 index 000000000000..ada5baf0b60d --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force.fail @@ -0,0 +1 @@ +test_cbmc_options="-DFORCE_FAILURE" diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail new file mode 100644 index 000000000000..8fe00c8db466 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail @@ -0,0 +1 @@ +test_cbmc_options="-DFORCE_FAILURE_2" diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail new file mode 100644 index 000000000000..612ed6772844 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force3.fail @@ -0,0 +1 @@ +test_cbmc_options="-DFORCE_FAILURE_3" diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass new file mode 100644 index 000000000000..e69de29bb2d1 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/main.pass diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c new file mode 100644 index 000000000000..470b1105a112 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c @@ -0,0 +1,72 @@ +#include <src/combined_source.c> + +int x; +int y; + +int __unbuffered_tpr_x; +int __unbuffered_tpr_y; + +DEFINE_SRCU(ss); + +void rcu_reader(void) +{ + int idx; + +#ifndef FORCE_FAILURE_3 + idx = srcu_read_lock(&ss); +#endif + might_sleep(); + + __unbuffered_tpr_y = READ_ONCE(y); +#ifdef FORCE_FAILURE + srcu_read_unlock(&ss, idx); + idx = srcu_read_lock(&ss); +#endif + WRITE_ONCE(x, 1); + +#ifndef FORCE_FAILURE_3 + srcu_read_unlock(&ss, idx); +#endif + might_sleep(); +} + +void *thread_update(void *arg) +{ + WRITE_ONCE(y, 1); +#ifndef FORCE_FAILURE_2 + synchronize_srcu(&ss); +#endif + might_sleep(); + __unbuffered_tpr_x = READ_ONCE(x); + + return NULL; +} + +void *thread_process_reader(void *arg) +{ + rcu_reader(); + + return NULL; +} + +int main(int argc, char *argv[]) +{ + pthread_t tu; + pthread_t tpr; + + if (pthread_create(&tu, NULL, thread_update, NULL)) + abort(); + if (pthread_create(&tpr, NULL, thread_process_reader, NULL)) + abort(); + if (pthread_join(tu, NULL)) + abort(); + if (pthread_join(tpr, NULL)) + abort(); + assert(__unbuffered_tpr_y != 0 || __unbuffered_tpr_x != 0); + +#ifdef ASSERT_END + assert(0); +#endif + + return 0; +} |