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
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 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.
+
* Algorithm verified :
*
- * 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;
+ * 1 waiter
+ *
* while (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) { };
+ * }
+ * }
* }
- * queue = 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
int queue[2] = 0;
int waiting[2] = 0;
+int futex = 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);
- do
- :: 1 ->
- queue[get_pid()] = gp;
-
+ /* loop 1 */
+ queue[get_pid()] = 1;
+
+ if
+ :: (futex == -1) ->
if
- :: (waiting[get_pid()] == 1) ->
+ :: (waiting[get_pid() == 1]) ->
waiting[get_pid()] = 0;
- 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;
fi;
- od;
+ :: 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()
{
-restart:
- in_registry[0] = 1;
- in_registry[1] = 1;
do
:: 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;
#endif
- 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;
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) ->
- 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;
#endif
+ 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;
od;
+
}
projects / userspace-rcu.git / commitdiff
