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

DEFINITIONS

1. rcu_reader
2. thread_update
3. thread_process_reader
4. main

   1 // SPDX-License-Identifier: GPL-2.0
   2 #include <src/combined_source.c>
   3 
   4 int x;
   5 int y;
   6 
   7 int __unbuffered_tpr_x;
   8 int __unbuffered_tpr_y;
   9 
  10 DEFINE_SRCU(ss);
  11 
  12 void 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 
  34 void *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 
  46 void *thread_process_reader(void *arg)
  47 {
  48         rcu_reader();
  49 
  50         return NULL;
  51 }
  52 
  53 int 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 }