- WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
- :: else ->
- WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1);
- fi;
+ 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;
+