projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
update
[urcu.git]
/
ticketlock-testwait
/
mem-progress.spin
diff --git
a/ticketlock-testwait/mem-progress.spin
b/ticketlock-testwait/mem-progress.spin
index 818f445a74872642af1cadfd92f5998ba7e62b34..8329f6b8cbfd18343672b51c02d62c5ff6d80142 100644
(file)
--- a/
ticketlock-testwait/mem-progress.spin
+++ b/
ticketlock-testwait/mem-progress.spin
@@
-40,6
+40,10
@@
byte refcount = 0;
#define need_pause() (_pid == 2)
#define need_pause() (_pid == 2)
+/*
+ * do_pause() disabled:
+ * get similar effect by disabling weak fairness.
+ */
/*
* Test weak fairness by either not pausing or cycling for any number of
* steps, or forever.
/*
* Test weak fairness by either not pausing or cycling for any number of
* steps, or forever.
@@
-54,15
+58,11
@@
inline do_pause()
{
if
:: need_pause() ->
{
if
:: need_pause() ->
- if
+ do
:: 1 ->
:: 1 ->
- do
- :: 1 ->
- skip;
- od;
- :: 1 -> skip;
- fi;
- :: else ->
+ skip;
+ od;
+ :: 1 ->
skip;
fi;
}
skip;
fi;
}
@@
-110,10
+110,11
@@
proctype proc_B()
do
:: 1 ->
do
:: 1 ->
- do_pause();
+progress_B:
+ //do_pause();
spin_lock(lock, ticket);
refcount = refcount + 1;
spin_lock(lock, ticket);
refcount = refcount + 1;
- do_pause();
+
//
do_pause();
refcount = refcount - 1;
spin_unlock(lock);
od;
refcount = refcount - 1;
spin_unlock(lock);
od;
This page took
0.02291 seconds
and
4
git commands to generate.