The nto1 selective wakeup model introduced by Paolo was:
a) too complex (tried to model the full-blown RCU rather than a simple
queue system)
b) did not model progress with wakers running for a limited amount of
iterations, only with wakers running infinitely often (which
therefore does not prove anything).
What we really want to model here is what happens if we have wakers
running a few times, and then not running for a very long time: can we
end up with a missed wakeup, and therefore end up with an enqueued entry
but with the waiter waiting forever ?
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
-/* no defines needed yet */
+#define queue_has_entry (queue[0] == 1 || queue[1] == 1)
make futex_progress | tee futex_progress.log
make futex_progress_no_wake | tee futex_progress_no_wake.log
make futex_progress_late_dec | tee futex_progress_late_dec.log
make futex_progress | tee futex_progress.log
make futex_progress_no_wake | tee futex_progress_no_wake.log
make futex_progress_late_dec | tee futex_progress_late_dec.log
- make futex_progress_inverted_waiting_vs_gp_futex | tee futex_progress_inverted_waiting_vs_gp_futex.define.log
make asserts | tee asserts.log
make summary
make asserts | tee asserts.log
make summary
futex_progress_late_dec_define:
cp futex_progress_late_dec.define .input.define
futex_progress_late_dec_define:
cp futex_progress_late_dec.define .input.define
-futex_progress_inverted_waiting_vs_gp_futex: clean futex_ltl futex_progress_inverted_waiting_vs_gp_futex_define run_weak_fair
- cp .input.spin $@.spin.input
- -cp .input.spin.trail $@.spin.input.trail
-
-futex_progress_inverted_waiting_vs_gp_futex_define:
- cp futex_progress_inverted_waiting_vs_gp_futex.define .input.define
-
futex_ltl:
touch .input.define
cat DEFINES > pan.ltl
futex_ltl:
touch .input.define
cat DEFINES > pan.ltl
+([] <> ((!np_) || (!queue_has_entry)))
* futex wakeup algorithm.
*
* In this model, waker threads are told whether they are still being
* futex wakeup algorithm.
*
* In this model, waker threads are told whether they are still being
- * waited on, and skip the futex wakeup if not.
- *
+ * waited on, and skip the futex wakeup if not. The waiter progresses
+ * each time it sees data in both queues.
+
- * queue = 0;
- * waiting = 0;
- * gp_futex = 0;
- * gp = 1;
+ * queue[n] = 0;
+ * futex = 0;
+ * futex_wake = 0;
- * Waker
- * while (1) {
- * this.queue = gp;
- * if (this.waiting == 1) {
- * this.waiting = 0;
- * if (gp_futex == -1) {
- * gp_futex = 0;
- * futex_wake = 1;
- * }
+ * n wakers (2 loops)
+ *
+ * queue[pid] = 1;
+ * if (futex == -1) {
+ * if (waker[pid].waiting == 1) {
+ * waker[pid].waiting = 0;
+ * futex = 0;
+ * futex_wake = 1;
- * Waiter
- * in_registry = 1;
- * gp_futex = -1;
- * waiting |= (queue != gp);
- * in_registry &= (queue != gp);
- * if (all in_registry == 0) {
- * progress:
- * gp_futex = 0;
- * gp = !gp;
- * restart;
- * } else {
- * futex_wake = (gp_futex == -1 ? 0 : 1);
- * while (futex_wake == 0) { }
+ * futex = -1;
+ * waker[0].waiting = 1;
+ * waker[1].waiting = 1;
+ * while (!(queue[0] == 1 && queue[1] == 1)) {
+ * if (futex == -1) {
+ * futex_wake = (futex == -1 ? 0 : 1); (atomic)
+ * while (futex_wake == 0) { };
+ * }
+ * }
+ * futex = 0;
+ * waker[0].waiting = 0;
+ * waker[1].waiting = 0;
+ * progress:
+ * queue[0] = 0;
+ * queue[1] = 0;
- * 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.
+ * if queue = 1, then !_np
+ *
+ * By testing progress, i.e. [] <> ((!np_) || (!queue_has_entry)), we
+ * check that we can never block forever if there is an entry in the
+ * any of the queues.
+ *
+ * The waker performs only 2 loops (and NOT an infinite number of loops)
+ * because we really want to see what happens when the waker stops
+ * enqueuing.
*
* 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
int queue[2] = 0;
int waiting[2] = 0;
int queue[2] = 0;
int waiting[2] = 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);
- do
- :: 1 ->
- queue[get_pid()] = gp;
-
+ /* loop 1 */
+ queue[get_pid()] = 1;
+
+ if
+ :: (futex == -1) ->
- :: (waiting[get_pid()] == 1) ->
+ :: (waiting[get_pid() == 1]) ->
- if
- :: (gp_futex == -1) ->
- gp_futex = 0;
-#ifndef INJ_QUEUE_NO_WAKE
- futex_wake = 1;
-#endif
- :: else ->
- skip;
- fi;
+ futex = 0;
+ futex_wake = 1;
+ :: else -> skip;
+ :: else ->
+ skip;
+ fi;
+
+ /* loop 2 */
+ queue[get_pid()] = 1;
+
+ if
+ :: (futex == -1) ->
+ if
+ :: (waiting[get_pid() == 1]) ->
+ waiting[get_pid()] = 0;
+ futex = 0;
+ futex_wake = 1;
+ :: else -> skip;
+ fi;
+ :: else ->
+ skip;
+ fi;
+
+#ifdef INJ_QUEUE_NO_WAKE
+ /* loop 3 */
+ queue[get_pid()] = 1;
+#endif
}
active proctype waiter()
{
}
active proctype waiter()
{
-restart:
- in_registry[0] = 1;
- in_registry[1] = 1;
-#if (!defined(INJ_LATE_DEC) && !defined(INJ_INVERT_WAITING_VS_GP_FUTEX))
- gp_futex = -1;
+#ifndef INJ_LATE_DEC
+ futex = -1;
+ waiting[0] = 1;
+ waiting[1] = 1;
- if
- :: (in_registry[0] == 1 && queue[0] != gp) ->
+
+ do
+ :: 1 ->
+ if
+ :: (queue[0] == 1 || queue[1] == 1) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+#ifdef INJ_LATE_DEC
+ futex = -1;
- :: else ->
- skip;
- fi;
- if
- :: (in_registry[1] == 1 && queue[1] != gp) ->
- :: else ->
- skip;
- fi;
-
- if
- :: (in_registry[0] == 1 && queue[0] == gp) ->
- in_registry[0] = 0;
- :: else ->
- skip;
- fi;
- if
- :: (in_registry[1] == 1 && queue[1] == gp) ->
- in_registry[1] = 0;
- :: else ->
- skip;
- fi;
-#ifdef INJ_INVERT_WAITING_VS_GP_FUTEX
- gp_futex = -1;
+ if
+ :: (futex == -1) ->
+ atomic {
+ if
+ :: (futex == -1) ->
+ futex_wake = 0;
+ :: else ->
+ futex_wake = 1;
+ fi;
+ }
+ /* block */
+ do
+ :: 1 ->
+ if
+ :: (futex_wake == 0) ->
+ skip;
+ :: else ->
+ break;
+ fi;
+ od;
+ :: else ->
+ skip;
+ fi;
+ od;
- if
- :: (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;
+ futex = 0;
+ waiting[0] = 0;
+ waiting[1] = 0;
+progress: /* progress on dequeue */
+ queue[0] = 0;
+ queue[1] = 0;
+++ /dev/null
-#define INJ_INVERT_WAITING_VS_GP_FUTEX