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.
---
futex-wakeup/futex.spin | 40 +++++++++++++++++++++++++++++++---------
1 files changed, 31 insertions(+), 9 deletions(-)
diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
index ab41a0a..44acd7e 100644
--- a/futex-wakeup/futex.spin
+++ b/futex-wakeup/futex.spin
@@ -9,9 +9,12 @@
* 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;
+ * }
* }
* }
*
@@ -19,6 +22,7 @@
* in_registry = 1;
* while (1) {
* gp_futex = -1;
+ * waiting |= (queue != gp);
* in_registry &= (queue != gp);
* if (all in_registry == 0) {
* progress:
@@ -56,6 +60,7 @@
#define get_pid() (_pid)
int queue[2] = 0;
+int waiting[2] = 0;
int futex_wake = 0;
int gp_futex = 0;
int gp = 1;
@@ -69,14 +74,18 @@ active [2] proctype waker()
:: 1 ->
queue[get_pid()] = gp;
- if
- :: (gp_futex == -1) ->
- gp_futex = 0;
+ if
+ :: (waiting[get_pid()] == 1) ->
+ waiting[get_pid()] = 0;
+ if
+ :: (gp_futex == -1) ->
+ gp_futex = 0;
#ifndef INJ_QUEUE_NO_WAKE
- futex_wake = 1;
+ futex_wake = 1;
#endif
- :: else ->
- skip;
+ :: else ->
+ skip;
+ fi;
fi;
od;
}
@@ -92,6 +101,18 @@ restart:
#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) ->
@@ -105,6 +126,7 @@ restart:
:: else ->
skip;
fi;
+
if
:: (in_registry[0] == 0 && in_registry[1] == 0) ->
progress:
--
1.7.6
_______________________________________________
ltt-dev mailing list
[email protected]
http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
