* Paolo Bonzini ([email protected]) wrote:
> Rewrite the model to include the futex primitives and the list
> move algorithm used by urcu. The model implements a full-blown
> parity-flipping RCU where grace period waits are driven exclusively
> by futexes. It runs the waker and waiter infinitely, asserting
> that progress states (parity flips) are reached infinite times.
merged, thanks!!
Mathieu
> ---
> futex-wakeup/DEFINES | 2 +-
> futex-wakeup/futex.ltl | 2 +-
> futex-wakeup/futex.spin | 134
> +++++++++++++++++++++++++----------------------
> 3 files changed, 73 insertions(+), 65 deletions(-)
>
> diff --git a/futex-wakeup/DEFINES b/futex-wakeup/DEFINES
> index e328b55..3e0a545 100644
> --- a/futex-wakeup/DEFINES
> +++ b/futex-wakeup/DEFINES
> @@ -1 +1 @@
> -#define queue_has_entry (queue[0] == 1 || queue[1] == 1)
> +/* no defines needed yet */
> diff --git a/futex-wakeup/futex.ltl b/futex-wakeup/futex.ltl
> index 3d6842e..8718641 100644
> --- a/futex-wakeup/futex.ltl
> +++ b/futex-wakeup/futex.ltl
> @@ -1 +1 @@
> -([] <> ((!np_) || (!queue_has_entry)))
> +([] <> !np_)
> diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
> index 5459a53..ab41a0a 100644
> --- a/futex-wakeup/futex.spin
> +++ b/futex-wakeup/futex.spin
> @@ -4,30 +4,39 @@
> * 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
> + * in_registry = 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 {
> - * if (fut == -1) {
> - * while (fut == -1) { }
> - * }
> + * futex_wake = (gp_futex == -1 ? 0 : 1);
> + * while (futex_wake == 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
> @@ -49,76 +56,77 @@
> #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);
>
> - 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
> + :: else ->
> + skip;
> + fi;
> + od;
> }
>
>
> active proctype waiter()
> {
> +restart:
> + in_registry[0] = 1;
> + in_registry[1] = 1;
> do
> :: 1 ->
> #ifndef INJ_LATE_DEC
> - fut = fut - 1;
> + gp_futex = -1;
> #endif
> +
> 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 ->
> -#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;
> -progress:
> if
> - :: queue[0] == 1 ->
> - queue[0] = 0;
> + :: (in_registry[1] == 1 && queue[1] == gp) ->
> + in_registry[1] = 0;
> + :: else ->
> + skip;
> 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;
> }
> --
> 1.7.6
>
>
>
> _______________________________________________
> ltt-dev mailing list
> [email protected]
> http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
>
--
Mathieu Desnoyers
Operating System Efficiency R&D Consultant
EfficiOS Inc.
http://www.efficios.com
_______________________________________________
ltt-dev mailing list
[email protected]
http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
