projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Revert "spinlock model: Simplify state-space"
[urcu.git]
/
spinlock
/
mem.spin
diff --git
a/spinlock/mem.spin
b/spinlock/mem.spin
index db8a8b3b66247edcd1e1bd9656fa2597b5c990ae..9e87809ea64998947cb27f6b6c88745019f0e2e8 100644
(file)
--- a/
spinlock/mem.spin
+++ b/
spinlock/mem.spin
@@
-21,7
+21,17
@@
byte refcount = 0;
inline spin_lock(lock)
{
inline spin_lock(lock)
{
- atomic { !lock -> lock = 1 }
+ do
+ :: 1 -> atomic {
+ if
+ :: (lock) ->
+ skip;
+ :: else ->
+ lock = 1;
+ break;
+ fi;
+ }
+ od;
}
inline spin_unlock(lock)
}
inline spin_unlock(lock)
@@
-32,7
+42,8
@@
inline spin_unlock(lock)
proctype proc_X()
{
do
proctype proc_X()
{
do
- :: spin_lock(lock);
+ :: 1 ->
+ spin_lock(lock);
refcount = refcount + 1;
refcount = refcount - 1;
spin_unlock(lock);
refcount = refcount + 1;
refcount = refcount - 1;
spin_unlock(lock);
This page took
0.023555 seconds
and
4
git commands to generate.