X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2Furcu.spin;fp=formal-model%2Furcu%2Furcu.spin;h=f4d3ea78ade593788bf9d97710e7c8bda5ace2ff;hb=a570e118a8f9ed38d5eaebf8d21b65d2b6f5cf40;hp=570da40231773d139e2c80166b584b0585136da3;hpb=6ae334b09959594326f5d85f76e0427c03a64995;p=urcu.git

diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index 570da40..f4d3ea7 100644
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -212,6 +212,7 @@ inline wait_for_reader(tmp, id, i)
 	:: 1 ->
 		ooo_mem(i);
 		tmp = READ_CACHED_VAR(urcu_active_readers_one);
+		ooo_mem(i);
 		if
 		:: (tmp & RCU_GP_CTR_NEST_MASK)
 			&& ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr))