inline spin_lock(lock)
{
- atomic{ !lock -> lock = 1}
+ do
+ :: 1 -> atomic {
+ if
+ :: (lock) ->
+ skip;
+ :: else ->
+ lock = 1;
+ break;
+ fi;
+ }
+ od;
}
inline spin_unlock(lock)
proctype proc_X()
{
do
- :: spin_lock(lock);
+ :: 1 ->
+ spin_lock(lock);
refcount = refcount + 1;
refcount = refcount - 1;
spin_unlock(lock);