projects
/
userspace-rcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
add missing ooo_mem() to writer model
[userspace-rcu.git]
/
formal-model
/
urcu
/
urcu.spin
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))
This page took
0.022693 seconds
and
4
git commands to generate.