From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Thu, 19 Mar 2009 19:13:12 +0000 (-0400)
Subject: add missing ooo_mem() to writer model
X-Git-Tag: v0.1~268
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=a570e118a8f9ed38d5eaebf8d21b65d2b6f5cf40;p=userspace-rcu.git

add missing ooo_mem() to writer model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
---

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))