[ltt-dev] [[PATCH URCU formal]] Restructure urcu_updater() to more accurately reflect actual failure scenario.

[Mathieu Desnoyers]

* Paul E. McKenney (paulmck at linux.vnet.ibm.com) wrote:
> Restructure urcu_updater() to more accurately reflect actual failure
> scenario.
> 
> This allows an easier transformation to force failure -- simple #ifdef
> out the second counter flip out of urcu_updater()'s model of
> "current synchronize_rcu()".
> 

Merged, thanks !

Mathieu

> Signed-off-by: Paul E. McKenney <paulmck at linux.vnet.ibm.com>
> ---
>  formal-model/urcu.spin |   41 +++++++++++++++++++++++++++++++----------
>  1 files changed, 31 insertions(+), 10 deletions(-)
> 
> diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
> index eea18e8..3e18457 100644
> --- a/formal-model/urcu.spin
> +++ b/formal-model/urcu.spin
> @@ -187,10 +187,38 @@ proctype urcu_reader()
>  
>  proctype urcu_updater()
>  {
> +	/* prior synchronize_rcu(), second counter flip. */
> +	need_mb = 1;
> +	do
> +	:: need_mb == 1 -> skip;
> +	:: need_mb == 0 -> break;
> +	od;
> +	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> +	need_mb = 1;
> +	do
> +	:: need_mb == 1 -> skip;
> +	:: need_mb == 0 -> break;
> +	od;
> +	do
> +	:: 1 ->
> +		if
> +		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
> +		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
> +		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
> +			skip;
> +		:: else -> break;
> +		fi;
> +	od;
> +	need_mb = 1;
> +	do
> +	:: need_mb == 1 -> skip;
> +	:: need_mb == 0 -> break;
> +	od;
> +
>  	/* Removal statement, e.g., list_del_rcu(). */
>  	removed = 1;
>  
> -	/* synchronize_rcu(), first counter flip. */
> +	/* current synchronize_rcu(), first counter flip. */
>  	need_mb = 1;
>  	do
>  	:: need_mb == 1 -> skip;
> @@ -204,15 +232,13 @@ proctype urcu_updater()
>  	od;
>  	do
>  	:: 1 ->
> -		printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
> -		printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
>  		if
>  		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
>  		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
>  		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
>  			skip;
>  		:: else -> break;
> -		fi
> +		fi;
>  	od;
>  	need_mb = 1;
>  	do
> @@ -220,10 +246,7 @@ proctype urcu_updater()
>  	:: need_mb == 0 -> break;
>  	od;
>  
> -	/* Erroneous removal statement, e.g., list_del_rcu(). */
> -	/* removed = 1; */
> -
> -	/* synchronize_rcu(), second counter flip. */
> +	/* current synchronize_rcu(), second counter flip. */
>  	need_mb = 1;
>  	do
>  	:: need_mb == 1 -> skip;
> @@ -237,8 +260,6 @@ proctype urcu_updater()
>  	od;
>  	do
>  	:: 1 ->
> -		printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
> -		printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
>  		if
>  		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
>  		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
> -- 
> 1.5.2.5
> 

-- 
Mathieu Desnoyers
OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F  BA06 3F25 A8FE 3BAE 9A68