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

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

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