projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
dual writer fix
[urcu.git]
/
formal-model
/
urcu
/
urcu.spin
diff --git
a/formal-model/urcu/urcu.spin
b/formal-model/urcu/urcu.spin
index 7f94d3b10232b7ff91520852a65d7236238f5385..5ac2f02dd9d80c3abd8d08f2b20136dd9a604635 100644
(file)
--- a/
formal-model/urcu/urcu.spin
+++ b/
formal-model/urcu/urcu.spin
@@
-225,11
+225,16
@@
active [NR_WRITERS] proctype urcu_writer()
ooo_mem(i);
do
ooo_mem(i);
do
- :: write_lock == 0 ->
- write_lock = 1;
- break;
- :: else ->
- skip;
+ :: 1 ->
+ atomic {
+ if
+ :: write_lock == 0 ->
+ write_lock = 1;
+ break;
+ :: else ->
+ skip;
+ fi;
+ }
od;
smp_mb(i);
ooo_mem(i);
od;
smp_mb(i);
ooo_mem(i);
@@
-251,11
+256,11
@@
active [NR_WRITERS] proctype urcu_writer()
#endif
ooo_mem(i);
smp_mb(i);
#endif
ooo_mem(i);
smp_mb(i);
- /* free-up step, e.g., kfree(). */
ooo_mem(i);
ooo_mem(i);
+ write_lock = 0;
+ /* free-up step, e.g., kfree(). */
atomic {
last_free_gen = old_gen;
free_done = 1;
atomic {
last_free_gen = old_gen;
free_done = 1;
- write_lock = 0;
}
}
}
}
This page took
0.02286 seconds
and
4
git commands to generate.