This patch adds to the model an optimization, whereby threads are
told whether they are still being waited on, and skip the futex wakeup
if not.
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
* Waker
* while (1) {
* this.queue = gp;
* Waker
* while (1) {
* this.queue = gp;
- * if (gp_futex == -1) {
- * gp_futex = 0;
- * futex_wake = 1;
+ * if (this.waiting == 1) {
+ * this.waiting = 0;
+ * if (gp_futex == -1) {
+ * gp_futex = 0;
+ * futex_wake = 1;
+ * }
* in_registry = 1;
* while (1) {
* gp_futex = -1;
* in_registry = 1;
* while (1) {
* gp_futex = -1;
+ * waiting |= (queue != gp);
* in_registry &= (queue != gp);
* if (all in_registry == 0) {
* progress:
* in_registry &= (queue != gp);
* if (all in_registry == 0) {
* progress:
#define get_pid() (_pid)
int queue[2] = 0;
#define get_pid() (_pid)
int queue[2] = 0;
int futex_wake = 0;
int gp_futex = 0;
int gp = 1;
int futex_wake = 0;
int gp_futex = 0;
int gp = 1;
queue[get_pid()] = gp;
if
queue[get_pid()] = gp;
if
- :: (gp_futex == -1) ->
- gp_futex = 0;
+ :: (waiting[get_pid()] == 1) ->
+ waiting[get_pid()] = 0;
+ if
+ :: (gp_futex == -1) ->
+ gp_futex = 0;
#ifndef INJ_QUEUE_NO_WAKE
#ifndef INJ_QUEUE_NO_WAKE
+ :: else ->
+ skip;
+ fi;
#ifndef INJ_LATE_DEC
gp_futex = -1;
#endif
#ifndef INJ_LATE_DEC
gp_futex = -1;
#endif
+ if
+ :: (in_registry[0] == 1 && queue[0] != gp) ->
+ waiting[0] = 1;
+ :: else ->
+ skip;
+ fi;
+ if
+ :: (in_registry[1] == 1 && queue[1] != gp) ->
+ waiting[1] = 1;
+ :: else ->
+ skip;
+ fi;
if
:: (in_registry[0] == 1 && queue[0] == gp) ->
if
:: (in_registry[0] == 1 && queue[0] == gp) ->
if
:: (in_registry[0] == 0 && in_registry[1] == 0) ->
progress:
if
:: (in_registry[0] == 0 && in_registry[1] == 0) ->
progress: