diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-27 10:05:51 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-27 10:05:51 +0000 |
commit | 5d1646d90e1f2cceb9f0828f4b28318cd0ec7744 (patch) | |
tree | a94efe259b9009378be6d90eb30d2b019d95c194 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c | |
parent | Initial commit. (diff) | |
download | linux-5d1646d90e1f2cceb9f0828f4b28318cd0ec7744.tar.xz linux-5d1646d90e1f2cceb9f0828f4b28318cd0ec7744.zip |
Adding upstream version 5.10.209.upstream/5.10.209upstream
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c | 73 |
1 files changed, 73 insertions, 0 deletions
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 000000000..2ce2016f7 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c @@ -0,0 +1,73 @@ +// SPDX-License-Identifier: GPL-2.0 +#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; +} |