+#ifndef TEST_SIGNAL_ON_WRITE
+
+inline urcu_one_read(i, j, nest_i, tmp, tmp2)
+{
+ nest_i = 0;
+ do
+ :: nest_i < READER_NEST_LEVEL ->
+ ooo_mem(i);
+ dispatch_sighand_read_exec();
+ tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
+ ooo_mem(i);
+ dispatch_sighand_read_exec();
+ if
+ :: (!(tmp & RCU_GP_CTR_NEST_MASK))
+ ->
+ tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
+ ooo_mem(i);
+ dispatch_sighand_read_exec();
+ WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
+ tmp2);
+ :: else ->
+ WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
+ tmp + 1);
+ fi;
+ smp_mb_reader(i, j);
+ dispatch_sighand_read_exec();
+ nest_i++;
+ :: nest_i >= READER_NEST_LEVEL -> break;
+ od;
+
+ read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
+ data_access[get_readerid()] = 1;
+ data_access[get_readerid()] = 0;
+
+ nest_i = 0;
+ do
+ :: nest_i < READER_NEST_LEVEL ->
+ smp_mb_reader(i, j);
+ dispatch_sighand_read_exec();
+ tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
+ ooo_mem(i);
+ dispatch_sighand_read_exec();
+ WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
+ nest_i++;
+ :: nest_i >= READER_NEST_LEVEL -> break;
+ od;
+ //ooo_mem(i);
+ //dispatch_sighand_read_exec();
+ //smp_mc(i); /* added */
+}
+
+active proctype urcu_reader()