+ //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
+ /* Only test progress of one random reader. They are all the
+ * same. */
+ if
+ :: get_readerid() == 0 ->
+progress_reader:
+ skip;
+ fi;
+#endif
+ urcu_one_read(i, j, nest_i, tmp, tmp2);
+ od;
+}