+ /* prior synchronize_rcu(), second counter flip. */
+ need_mb = 1;
+ do
+ :: need_mb == 1 -> skip;
+ :: need_mb == 0 -> break;
+ od;
+ urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
+ need_mb = 1;
+ do
+ :: need_mb == 1 -> skip;
+ :: need_mb == 0 -> break;
+ od;
+ do
+ :: 1 ->
+ if
+ :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
+ (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
+ (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
+ skip;
+ :: else -> break;
+ fi;
+ od;
+ need_mb = 1;
+ do
+ :: need_mb == 1 -> skip;
+ :: need_mb == 0 -> break;
+ od;
+