* Copyright (c) 2009 Mathieu Desnoyers
*/
-int queue = 0;
+#define get_pid() (_pid)
+
+int queue[2] = 0;
int fut = 0;
-active proctype waker()
+active [2] proctype waker()
{
- queue = 1;
+ assert(get_pid() < 2);
+
+ queue[get_pid()] = 1;
if
:: (fut == -1) ->
skip;
fi;
- queue = 1;
+ queue[get_pid()] = 1;
if
:: (fut == -1) ->
fi;
#ifdef INJ_QUEUE_NO_WAKE
- queue = 1;
+ queue[get_pid()] = 1;
#endif
}
fut = fut - 1;
#endif
if
- :: (queue == 1) ->
+ :: (queue[0] == 1 || queue[1] == 1) ->
#ifndef INJ_LATE_DEC
fut = 0;
#endif
:: 1 ->
if
:: (fut == -1) ->
- if
- :: (queue == 0) ->
-progress_A:
- skip;
- :: else
- skip;
- fi;
skip;
:: else ->
break;
skip;
fi;
fi;
-progress_B:
- queue = 0;
+progress:
+ if
+ :: queue[0] == 1 ->
+ queue[0] = 0;
+ fi;
+ if
+ :: queue[1] == 1 ->
+ queue[1] = 0;
+ fi;
od;
}