[ltt-dev] [PATCH v2 2/3] model optimization of the waker (selective wake)

[Mathieu Desnoyers]

* Paolo Bonzini (pbonzini at redhat.com) wrote:
> This patch adds to the model an optimization, whereby threads are
> told whether they are still being waited on, and skip the futex wakeup
> if not.

Merged, thanks!

Mathieu

> ---
>  futex-wakeup/futex.spin |   40 +++++++++++++++++++++++++++++++---------
>  1 files changed, 31 insertions(+), 9 deletions(-)
> 
> diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
> index ab41a0a..44acd7e 100644
> --- a/futex-wakeup/futex.spin
> +++ b/futex-wakeup/futex.spin
> @@ -9,9 +9,12 @@
>   *                          Waker
>   *                          while (1) {
>   *                            this.queue = gp;
> - *                            if (gp_futex == -1) {
> - *                              gp_futex = 0;
> - *                              futex_wake = 1;
> + *                            if (this.waiting == 1) {
> + *                              this.waiting = 0;
> + *                              if (gp_futex == -1) {
> + *                                gp_futex = 0;
> + *                                futex_wake = 1;
> + *                              }
>   *                            }
>   *                          }
>   *
> @@ -19,6 +22,7 @@
>   * in_registry = 1;
>   * while (1) {
>   *   gp_futex = -1;
> + *   waiting |= (queue != gp);
>   *   in_registry &= (queue != gp);
>   *   if (all in_registry == 0) {
>   * progress:
> @@ -56,6 +60,7 @@
>  #define get_pid()       (_pid)
>  
>  int queue[2] = 0;
> +int waiting[2] = 0;
>  int futex_wake = 0;
>  int gp_futex = 0;
>  int gp = 1;
> @@ -69,14 +74,18 @@ active [2] proctype waker()
>  	:: 1 ->
>  		queue[get_pid()] = gp;
>  	
> -		if
> -		:: (gp_futex == -1) ->
> -			gp_futex = 0;
> +		if
> +		:: (waiting[get_pid()] == 1) ->
> +			waiting[get_pid()] = 0;
> +			if
> +			:: (gp_futex == -1) ->
> +				gp_futex = 0;
>  #ifndef INJ_QUEUE_NO_WAKE
> -			futex_wake = 1;
> +				futex_wake = 1;
>  #endif
> -		:: else ->
> -			skip;
> +			:: else ->
> +				skip;
> +			fi;
>  		fi;
>  	od;
>  }
> @@ -92,6 +101,18 @@ restart:
>  #ifndef INJ_LATE_DEC
>  		gp_futex = -1;
>  #endif
> +		if
> +		:: (in_registry[0] == 1 && queue[0] != gp) ->
> +			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) ->
> @@ -105,6 +126,7 @@ restart:
>  		:: else ->
>  			skip;
>  		fi;
> +
>  		if
>  		:: (in_registry[0] == 0 && in_registry[1] == 0) ->
>  progress:
> -- 
> 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