projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Cleanup promela code for wakeup verif
[urcu.git]
/
formal-model
/
futex-wakeup
/
futex.spin
diff --git
a/formal-model/futex-wakeup/futex.spin
b/formal-model/futex-wakeup/futex.spin
index 9f6ddd46cdcb11d838d31144f732452a08736d2e..1cb6442ace3a1d5f0df16d82ab2135d6e0b0317d 100644
(file)
--- a/
formal-model/futex-wakeup/futex.spin
+++ b/
formal-model/futex-wakeup/futex.spin
@@
-98,13
+98,6
@@
active proctype waiter()
:: 1 ->
if
:: (fut == -1) ->
:: 1 ->
if
:: (fut == -1) ->
- if
- :: (queue == 0) ->
-progress_A:
- skip;
- :: else
- skip;
- fi;
skip;
:: else ->
break;
skip;
:: else ->
break;
@@
-114,7
+107,7
@@
progress_A:
skip;
fi;
fi;
skip;
fi;
fi;
-progress
_B
:
+progress:
queue = 0;
od;
}
queue = 0;
od;
}
This page took
0.023252 seconds
and
4
git commands to generate.