linux-kernel - Re: [ltt-dev] [RFC git tree] Userspace RCU (urcu) for Linux (repost)

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]

Message-ID: <20090212023707.GA21193@linux.vnet.ibm.com>
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)