+#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()
+{
+ byte i, j, nest_i;
+ byte tmp, tmp2;
+
+ wait_init_done();
+
+ assert(get_pid() < NR_PROCS);
+
+end_reader:
+ do
+ :: 1 ->
+ /*
+ * We do not test reader's progress here, because we are mainly
+ * interested in writer's progress. The reader never blocks
+ * anyway. We have to test for reader/writer's progress
+ * separately, otherwise we could think the writer is doing
+ * progress when it's blocked by an always progressing reader.
+ */
+#ifdef READER_PROGRESS
+progress_reader:
+#endif
+ urcu_one_read(i, j, nest_i, tmp, tmp2);
+ od;
+}
+
+#endif //!TEST_SIGNAL_ON_WRITE
+
+#ifdef TEST_SIGNAL
+/* signal handler reader */
+
+inline urcu_one_read_sig(i, j, nest_i, tmp, tmp2)