linux-kernel - Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.

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: <20090221011856.GA21167@linux.vnet.ibm.com>
Date:	Fri, 20 Feb 2009 17:18:56 -0800
From:	"Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
To:	Mathieu Desnoyers <compudj@...stal.dyndns.org>
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] Add liveness checks to user-level RCU
	model.

On Fri, Feb 20, 2009 at 12:09:29PM -0800, Paul E. McKenney wrote:
> On Fri, Feb 20, 2009 at 02:46:21PM -0500, Mathieu Desnoyers wrote:

[ . . . ]

> > I'll first get the translation of asserts into LTL formulaes, and try to
> > see what should be fixed in the model. I have noticed that we would need
> > to do this :
> > 
> > urcu_gp_ctr = (urcu_gp_ctr + RCU_GP_CTR_BIT) % (RCU_GP_CTR_BIT + 1);
> > 
> > Otherwise the overflow does not do what we expect (spin -f on the trail
> > told me that it was overflowing to 1, which is not exactly what we want
> > I guess). More to come on that side. When this will be settled, I'll dig
> > further.
> 
> Hmmm...  The two legal values for urcu_gp_ctr are 1 and 129, so isn't
> this in fact the desired behavior?  This is with your optimization that
> cuts a half-cycle from rcu_read_lock() by making the initial value of
> urcu_gp_ctr be 1 rather than 0.
> 
> One way of getting rid of the warning would be something like the
> following:
> 
> 	atomic {
> 		if
> 		:: urcu_gp_ctr == 1 -> urcu_gp_ctr = 129;
> 		:: urcu_gp_ctr == 129 -> urcu_gp_ctr = 1;
> 		fi;
> 	}
> 
> On converting the assert() to LTL, better you than me!  :-)

Perhaps I should explain myself here...

Promela usually handles asserts() much more efficiently than it does LTL
or hand-code "never" clauses.  One reason is that "never" clauses act as
a separate Promela process that runs one step interleaved between every
step from any other process.  This obviously increases the run time, but
more importantly blows up the state space.

In addition, adding additional assert()s to a Promela program is easy to
do and has predictable consequences.  Combining a pair of LTL statements
is another thing altogether.

Of course, it is entirely possible that I would appreciate LTL more if
I were to use it more heavily.  ;-)

							Thanx, Paul
--
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/