tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c

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