From fda9aff00dcdf7cb49892d79f861d0acfb475514 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 11:59:42 -0400 Subject: [PATCH] Update nto1 selective model 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 --- futex-wakeup/nto1-selective/DEFINES | 2 +- futex-wakeup/nto1-selective/Makefile | 8 - futex-wakeup/nto1-selective/futex.ltl | 2 +- futex-wakeup/nto1-selective/futex.spin | 223 ++++++++++-------- ...ogress_inverted_waiting_vs_gp_futex.define | 1 - 5 files changed, 122 insertions(+), 114 deletions(-) delete mode 100644 futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define diff --git a/futex-wakeup/nto1-selective/DEFINES b/futex-wakeup/nto1-selective/DEFINES index 3e0a545..c6d28b2 100644 --- a/futex-wakeup/nto1-selective/DEFINES +++ b/futex-wakeup/nto1-selective/DEFINES @@ -1 +1 @@ -/* no defines needed yet */ +#define queue_has_entry (queue[0] == 1 || queue[1] == 1) diff --git a/futex-wakeup/nto1-selective/Makefile b/futex-wakeup/nto1-selective/Makefile index 2b6e243..11d98e8 100644 --- a/futex-wakeup/nto1-selective/Makefile +++ b/futex-wakeup/nto1-selective/Makefile @@ -29,7 +29,6 @@ default: 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 @@ -69,13 +68,6 @@ futex_progress_late_dec: clean futex_ltl futex_progress_late_dec_define run_weak 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 diff --git a/futex-wakeup/nto1-selective/futex.ltl b/futex-wakeup/nto1-selective/futex.ltl index 8718641..3d6842e 100644 --- a/futex-wakeup/nto1-selective/futex.ltl +++ b/futex-wakeup/nto1-selective/futex.ltl @@ -1 +1 @@ -([] <> !np_) +([] <> ((!np_) || (!queue_has_entry))) diff --git a/futex-wakeup/nto1-selective/futex.spin b/futex-wakeup/nto1-selective/futex.spin index 556f96f..6f854fc 100644 --- a/futex-wakeup/nto1-selective/futex.spin +++ b/futex-wakeup/nto1-selective/futex.spin @@ -3,48 +3,56 @@ * 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 @@ -67,97 +75,106 @@ 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; + } diff --git a/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define b/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define deleted file mode 100644 index eca05f6..0000000 --- a/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define +++ /dev/null @@ -1 +0,0 @@ -#define INJ_INVERT_WAITING_VS_GP_FUTEX -- 2.34.1