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] [thread-next>] [day] [month] [year] [list]
Date:	Wed, 11 Feb 2009 18:37:08 -0800
From:	"Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
To:	Mathieu Desnoyers <compudj@...stal.dyndns.org>
Cc:	ltt-dev@...ts.casi.polymtl.ca, linux-kernel@...r.kernel.org
Subject: Re: [ltt-dev] [RFC git tree] Userspace RCU (urcu) for Linux
	(repost)

On Wed, Feb 11, 2009 at 06:33:08PM -0800, Paul E. McKenney wrote:
> On Wed, Feb 11, 2009 at 04:35:49PM -0800, Paul E. McKenney wrote:
> > On Wed, Feb 11, 2009 at 04:42:58PM -0500, Mathieu Desnoyers wrote:
> > > * Paul E. McKenney (paulmck@...ux.vnet.ibm.com) wrote:

[ . . . ]

> > > > (BTW, I do not trust my model yet, as it currently cannot detect the
> > > > failure case I pointed out earlier.  :-/  Here and I thought that the
> > > > point of such models was to detect additional failure cases!!!)
> > > > 
> > > 
> > > Yes, I'll have to dig deeper into it.
> > 
> > Well, as I said, I attached the current model and the error trail.
> 
> And I had bugs in my model that allowed the rcu_read_lock() model
> to nest indefinitely, which overflowed into the top bit, messing
> things up.  :-/
> 
> Attached is a fixed model.  This model validates correctly (woo-hoo!).
> Even better, gives the expected error if you comment out line 180 and
> uncomment line 213, this latter corresponding to the error case I called
> out a few days ago.
> 
> I will play with removing models of mb...

And commenting out the models of mb between the counter flips and the
test for readers still passes validation, as expected, and as shown in
the attached Promela code.

						Thanx, Paul

View attachment "urcu.spin" of type "text/plain" (6413 bytes)

Powered by blists - more mailing lists