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 570da40231773d139e2c80166b584b0585136da3..f4d3ea78ade593788bf9d97710e7c8bda5ace2ff 100644 (file)
--- 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))