+inline urcu_one_read(i, nest_i, tmp, tmp2)
+{
+ nest_i = 0;
+ do
+ :: nest_i < READER_NEST_LEVEL ->
+ ooo_mem(i);
+ tmp = READ_CACHED_VAR(urcu_active_readers_one);
+ ooo_mem(i);
+ if
+ :: (!(tmp & RCU_GP_CTR_NEST_MASK))
+ ->
+ tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
+ ooo_mem(i);
+ WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
+ :: else ->
+ WRITE_CACHED_VAR(urcu_active_readers_one,
+ tmp + 1);
+ fi;
+ ooo_mem(i);
+ smp_mb(i);
+ nest_i++;
+ :: nest_i >= READER_NEST_LEVEL -> break;
+ od;
+
+ ooo_mem(i);
+ read_generation = READ_CACHED_VAR(generation_ptr);
+ ooo_mem(i);
+ data_access = 1;
+ ooo_mem(i);
+ data_access = 0;
+
+ nest_i = 0;
+ do
+ :: nest_i < READER_NEST_LEVEL ->
+ ooo_mem(i);
+ smp_mb(i);
+ ooo_mem(i);
+ tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
+ ooo_mem(i);
+ WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
+ nest_i++;
+ :: nest_i >= READER_NEST_LEVEL -> break;
+ od;
+ ooo_mem(i);
+ //smp_mc(i); /* added */
+}
+