lkml.org 
[lkml]   [2009]   [Feb]   [20]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH URCU formal] Add liveness checks to user-level RCU model.
* Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote:
> On Fri, Feb 20, 2009 at 01:18:35PM -0500, Mathieu Desnoyers wrote:
> > * Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote:
> > > Break all potentially infinite loops in both urcu_reader() and
> > > urcu_updater(), ensure that urcu_reader() will process any memory barriers
> > > that urcu_updater() might issue, and formulate a "never" claim that checks
> > > to make sure that if either urcu_reader() or urcu_updater() completes,
> > > then the other will eventually also complete. Since urcu_reader()
> > > now has a finite number of steps, it must eventually complete.
> > >
> > > Also replace the code at the end of urcu_reader() that previously absorbed
> > > late memory-barrier requests from urcu_updater with code in urcu_writer()
> > > that checks to see if urcu_reader() has completed.
> > >
> > > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >
> > Thanks Paul, I'll merge it. However, I am currently reworking our spin
> > tree so we can execute the tests in batch (rather that all at once,
> > which consumes more memory than necessary) and also I am doing a nice
> > build script which lets us create our own LTL formulaes for
> > verification. The never claims will be automatically generated and
> > verified. I'll keep you posted.
>
> Sounds interesting! Not sure what you mean by "execute the tests
> in batch", but look forward to seeing it.
>
> On the LTL, the formula "<>[] (reader_done != 0 && updater_done != 0)"
> didn't do what I want. The model would kick out an error with the
> reader sitting just before the "reader_done = 1" and the updater spinning
> waiting for the reader to respond to its memory-barrier request.
>
> So I fell back to the hand-coded formula in the never clause, which
> translates to English as "if either the reader or the updater complete,
> then both the reader and the updater eventually complete". There might
> be a way to tranlate that into LTL, but I didn't immediately see one.
>
> This morning I tried the weak fairness constraints (the "-f" argument
> to ./pan) and that did allow LTL to do what I want, as shown in the
> following patch (applied on top of my earlier patch).
>
> I must confess that LTL is at best an acquired taste for me.
> "Let's see... '<>[](!reader_done || !updater_done)'...
> That means eventually we always must have neither the reader or the
> updater being done. Huh??? Oh, yeah, this is supposed to say what
> -cannot- happen..." At this point, I have an easier time with the
> hand-coded "never" claims. ;-)
>
> But I am quite happy to leave further hacking on this model in
> your capable hands. The other item on my todo list was making the
> urcu_mbmin.spin model accurately handle omission of additional memory
> barriers. Are you willing to take that on as well?
>

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.

Mathieu


> Thanx, Paul
>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> ---
>
> urcu.sh | 4 ++--
> urcu.spin | 12 ------------
> 2 files changed, 2 insertions(+), 14 deletions(-)
>
> diff --git a/formal-model/urcu.sh b/formal-model/urcu.sh
> index 5e525ec..3a6850c 100644
> --- a/formal-model/urcu.sh
> +++ b/formal-model/urcu.sh
> @@ -20,6 +20,6 @@
> #
> # Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>
> -spin -a urcu.spin
> +spin -a -f '<>[](!reader_done || !updater_done)' urcu.spin
> cc -o pan pan.c
> -./pan -a
> +./pan -a -f
> diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
> index cf1f670..851eb50 100644
> --- a/formal-model/urcu.spin
> +++ b/formal-model/urcu.spin
> @@ -280,15 +280,3 @@ init {
> run urcu_updater();
> }
> }
> -
> -/* Require that both reader and updater eventually get done. */
> -
> -never {
> - do
> - :: skip;
> - :: reader_done != 0 || updater_done != 0 -> break;
> - od;
> -accept: do
> - :: reader_done == 0 || updater_done == 0;
> - od;
> -}
>

--
Mathieu Desnoyers
OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F BA06 3F25 A8FE 3BAE 9A68


\
 
 \ /
  Last update: 2009-02-20 20:49    [W:0.057 / U:0.584 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site