#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.
{
if
:: need_pause() ->
- if
+ do
:: 1 ->
- do
- :: 1 ->
- skip;
- od;
- :: 1 -> skip;
- fi;
- :: else ->
+ skip;
+ od;
+ :: 1 ->
skip;
fi;
}
do
:: 1 ->
- do_pause();
+progress_B:
+ //do_pause();
spin_lock(lock, ticket);
refcount = refcount + 1;
- do_pause();
+ //do_pause();
refcount = refcount - 1;
spin_unlock(lock);
od;