From a570e118a8f9ed38d5eaebf8d21b65d2b6f5cf40 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Thu, 19 Mar 2009 15:13:12 -0400 Subject: [PATCH] add missing ooo_mem() to writer model Signed-off-by: Mathieu Desnoyers --- formal-model/urcu/urcu.spin | 1 + 1 file changed, 1 insertion(+) 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)) -- 2.34.1