projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
new futex model
[urcu.git]
/
futex-wakeup
/
futex.spin
diff --git
a/futex-wakeup/futex.spin
b/futex-wakeup/futex.spin
index 5459a537b8f4b14f76bdde80eb8dddeb77548e2a..381174b1236950f03c3395e8aba27d53012079a9 100644
(file)
--- a/
futex-wakeup/futex.spin
+++ b/
futex-wakeup/futex.spin
@@
-4,30
+4,39
@@
* Algorithm verified :
*
* queue = 0;
* Algorithm verified :
*
* queue = 0;
- * fut = 0;
- * runvar = 0;
+ * waiting = 0;
+ * gp_futex = 0;
+ * gp = 1;
*
*
- * Waker
- * queue = 1;
- * if (fut == -1) {
- * fut = 0;
+ * Waker
+ * while (1) {
+ * this.queue = gp;
+ * if (gp_futex == -1) {
+ * gp_futex = 0;
+ * futex_wake = 1;
* }
* }
+ * }
*
* Waiter
*
* Waiter
+ * in_registry = 1;
* while (1) {
* while (1) {
- * progress:
- * fut = fut - 1;
- * if (queue == 1) {
- * fut = 0;
+ * gp_futex = -1;
+ * in_registry &= (queue != gp);
+ * if (all in_registry == 0) {
+ * progress:
+ * gp_futex = 0;
+ * gp = !gp;
+ * restart;
* } else {
* } else {
- * if (fut == -1) {
- * while (fut == -1) { }
- * }
+ * futex_wake = (gp_futex == -1 ? 0 : 1);
+ * while (futex_wake == 0) { }
* }
* queue = 0;
* }
*
* }
* queue = 0;
* }
*
- * if queue = 1, then !_np
+ * By testing progress, i.e. [] <> !np_, we check that an infinite sequence
+ * of update_counter_and_wait (and consequently of synchronize_rcu) will
+ * not block.
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
@@
-49,76
+58,77
@@
#define get_pid() (_pid)
int queue[2] = 0;
#define get_pid() (_pid)
int queue[2] = 0;
-int fut = 0;
+int futex_wake = 0;
+int gp_futex = 0;
+int gp = 1;
+int in_registry[2] = 0;
active [2] proctype waker()
{
assert(get_pid() < 2);
active [2] proctype waker()
{
assert(get_pid() < 2);
- queue[get_pid()] = 1;
-
- if
- :: (fut == -1) ->
- fut = 0;
- :: else ->
- skip;
- fi;
-
- queue[get_pid()] = 1;
-
- if
- :: (fut == -1) ->
- fut = 0;
- :: else ->
- skip;
- fi;
-
-#ifdef INJ_QUEUE_NO_WAKE
- queue[get_pid()] = 1;
+ do
+ :: 1 ->
+ queue[get_pid()] = gp;
+
+ if
+ :: (gp_futex == -1) ->
+ gp_futex = 0;
+#ifndef INJ_QUEUE_NO_WAKE
+ futex_wake = 1;
#endif
#endif
+ :: else ->
+ skip;
+ fi;
+ od;
}
active proctype waiter()
{
}
active proctype waiter()
{
+restart:
+ in_registry[0] = 1;
+ in_registry[1] = 1;
do
:: 1 ->
#ifndef INJ_LATE_DEC
do
:: 1 ->
#ifndef INJ_LATE_DEC
-
fut = fut -
1;
+
gp_futex = -
1;
#endif
#endif
+
if
if
- :: (queue[0] == 1 || queue[1] == 1) ->
-#ifndef INJ_LATE_DEC
- fut = 0;
-#endif
- skip;
+ :: (in_registry[0] == 1 && queue[0] == gp) ->
+ in_registry[0] = 0;
:: else ->
:: else ->
-#ifdef INJ_LATE_DEC
- fut = fut - 1;
-#endif
- if
- :: (fut == -1) ->
- do
- :: 1 ->
- if
- :: (fut == -1) ->
- skip;
- :: else ->
- break;
- fi;
- od;
- :: else ->
- skip;
- fi;
+ skip;
fi;
fi;
-progress:
if
if
- :: queue[0] == 1 ->
- queue[0] = 0;
+ :: (in_registry[1] == 1 && queue[1] == gp) ->
+ in_registry[1] = 0;
+ :: else ->
+ skip;
fi;
if
fi;
if
- :: queue[1] == 1 ->
- queue[1] = 0;
+ :: (in_registry[0] == 0 && in_registry[1] == 0) ->
+progress:
+#ifndef INJ_LATE_DEC
+ gp_futex = 0;
+#endif
+ gp = !gp;
+ goto restart;
+ :: else ->
+#ifdef INJ_LATE_DEC
+ gp_futex = -1;
+#endif
+ futex_wake = gp_futex + 1;
+ do
+ :: 1 ->
+ if
+ :: (futex_wake == 0) ->
+ skip;
+ :: else ->
+ break;
+ fi;
+ od;
fi;
od;
}
fi;
od;
}
This page took
0.02371 seconds
and
4
git commands to generate.