linux-kernel - Re: [[PATCH URCU formal]] Restructure urcu_updater() to more accurately reflect actual failure scenario.

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <20090220171526.GG1179@Krystal>
Date:	Fri, 20 Feb 2009 12:15:26 -0500
From:	Mathieu Desnoyers <compudj@...stal.dyndns.org>
To:	"Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
Cc:	ltt-dev@...ts.casi.polymtl.ca, bert.wesarg@...glemail.com,
	bob@...son.ibm.com, linux-kernel@...r.kernel.org
Subject: Re: [[PATCH URCU formal]] Restructure urcu_updater() to more
	accurately reflect actual failure scenario.

* Paul E. McKenney (paulmck@...ux.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@...ux.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
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/