projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
remove duplicate ooo_mem statements
[urcu.git]
/
formal-model
/
urcu
/
urcu.spin
diff --git
a/formal-model/urcu/urcu.spin
b/formal-model/urcu/urcu.spin
index f4d3ea78ade593788bf9d97710e7c8bda5ace2ff..324ee3945bd21507b11b49d9ab151230dcf0f0ed 100644
(file)
--- a/
formal-model/urcu/urcu.spin
+++ b/
formal-model/urcu/urcu.spin
@@
-29,7
+29,7
@@
/*
* Each process have its own data in cache. Caches are randomly updated.
/*
* Each process have its own data in cache. Caches are randomly updated.
- * smp_wmb and smp_rmb forces cache updates (write and read),
wmb
_mb forces
+ * smp_wmb and smp_rmb forces cache updates (write and read),
smp
_mb forces
* both.
*/
* both.
*/
@@
-113,7
+113,11
@@
inline smp_mb_pid(i)
#ifndef NO_RMB
smp_rmb_pid(i);
#endif
#ifndef NO_RMB
smp_rmb_pid(i);
#endif
- skip;
+#ifdef NO_WMB
+#ifdef NO_RMB
+ ooo_mem(i);
+#endif
+#endif
}
}
}
}
@@
-169,7
+173,11
@@
inline smp_mb(i)
#ifndef NO_RMB
smp_rmb(i);
#endif
#ifndef NO_RMB
smp_rmb(i);
#endif
- skip;
+#ifdef NO_WMB
+#ifdef NO_RMB
+ ooo_mem(i);
+#endif
+#endif
}
}
}
}
@@
-210,7
+218,6
@@
inline wait_for_reader(tmp, id, i)
{
do
:: 1 ->
{
do
:: 1 ->
- ooo_mem(i);
tmp = READ_CACHED_VAR(urcu_active_readers_one);
ooo_mem(i);
if
tmp = READ_CACHED_VAR(urcu_active_readers_one);
ooo_mem(i);
if
@@
-220,7
+227,7
@@
inline wait_for_reader(tmp, id, i)
#ifndef GEN_ERROR_WRITER_PROGRESS
smp_mb(i);
#else
#ifndef GEN_ERROR_WRITER_PROGRESS
smp_mb(i);
#else
-
skip
;
+
ooo_mem(i)
;
#endif
:: else ->
break;
#endif
:: else ->
break;
@@
-234,6
+241,12
@@
inline wait_for_quiescent_state(tmp, i, j)
do
:: i < NR_READERS ->
wait_for_reader(tmp, i, j);
do
:: i < NR_READERS ->
wait_for_reader(tmp, i, j);
+ if
+ :: (NR_READERS > 1) && (i < NR_READERS - 1)
+ -> ooo_mem(j);
+ :: else
+ -> skip;
+ fi;
i++
:: i >= NR_READERS -> break
od;
i++
:: i >= NR_READERS -> break
od;
@@
-259,7
+272,6
@@
inline urcu_one_read(i, nest_i, tmp, tmp2)
WRITE_CACHED_VAR(urcu_active_readers_one,
tmp + 1);
fi;
WRITE_CACHED_VAR(urcu_active_readers_one,
tmp + 1);
fi;
- ooo_mem(i);
smp_mb(i);
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
smp_mb(i);
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
@@
-275,9
+287,7
@@
inline urcu_one_read(i, nest_i, tmp, tmp2)
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
- ooo_mem(i);
smp_mb(i);
smp_mb(i);
- ooo_mem(i);
tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
@@
-347,7
+357,6
@@
progress_writer1:
}
od;
smp_mb(i);
}
od;
smp_mb(i);
- ooo_mem(i);
tmp = READ_CACHED_VAR(urcu_gp_ctr);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
tmp = READ_CACHED_VAR(urcu_gp_ctr);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
@@
-364,9
+373,7
@@
progress_writer1:
ooo_mem(i);
wait_for_quiescent_state(tmp, i, j);
#endif
ooo_mem(i);
wait_for_quiescent_state(tmp, i, j);
#endif
- ooo_mem(i);
smp_mb(i);
smp_mb(i);
- ooo_mem(i);
write_lock = 0;
/* free-up step, e.g., kfree(). */
atomic {
write_lock = 0;
/* free-up step, e.g., kfree(). */
atomic {
This page took
0.028014 seconds
and
4
git commands to generate.