LXR linux/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store

   1// SPDX-License-Identifier: GPL-2.0
   2#include <src/combined_source.c>
   3
   4int x;
   5int y;
   6
   7int __unbuffered_tpr_x;
   8int __unbuffered_tpr_y;
   9
  10DEFINE_SRCU(ss);
  11
  12void rcu_reader(void)
  13{
  14        int idx;
  15
  16#ifndef FORCE_FAILURE_3
  17        idx = srcu_read_lock(&ss);
  18#endif
  19        might_sleep();
  20
  21        __unbuffered_tpr_y = READ_ONCE(y);
  22#ifdef FORCE_FAILURE
  23        srcu_read_unlock(&ss, idx);
  24        idx = srcu_read_lock(&ss);
  25#endif
  26        WRITE_ONCE(x, 1);
  27
  28#ifndef FORCE_FAILURE_3
  29        srcu_read_unlock(&ss, idx);
  30#endif
  31        might_sleep();
  32}
  33
  34void *thread_update(void *arg)
  35{
  36        WRITE_ONCE(y, 1);
  37#ifndef FORCE_FAILURE_2
  38        synchronize_srcu(&ss);
  39#endif
  40        might_sleep();
  41        __unbuffered_tpr_x = READ_ONCE(x);
  42
  43        return NULL;
  44}
  45
  46void *thread_process_reader(void *arg)
  47{
  48        rcu_reader();
  49
  50        return NULL;
  51}
  52
  53int main(int argc, char *argv[])
  54{
  55        pthread_t tu;
  56        pthread_t tpr;
  57
  58        if (pthread_create(&tu, NULL, thread_update, NULL))
  59                abort();
  60        if (pthread_create(&tpr, NULL, thread_process_reader, NULL))
  61                abort();
  62        if (pthread_join(tu, NULL))
  63                abort();
  64        if (pthread_join(tpr, NULL))
  65                abort();
  66        assert(__unbuffered_tpr_y != 0 || __unbuffered_tpr_x != 0);
  67
  68#ifdef ASSERT_END
  69        assert(0);
  70#endif
  71
  72        return 0;
  73}
  74