[ltt-dev] [PATCH v2 1/3] new futex model

[Mathieu Desnoyers]

* Paolo Bonzini (pbonzini at redhat.com) 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
> ltt-dev at lists.casi.polymtl.ca
> 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