* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
@ 2009-02-20 18:18 Mathieu Desnoyers
2009-02-20 19:28 ` Paul E. McKenney
0 siblings, 1 reply; 9+ messages in thread
From: Mathieu Desnoyers @ 2009-02-20 18:18 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: ltt-dev, bert.wesarg, bob, linux-kernel
* 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.
Mathieu
> ---
> formal-model/urcu.sh | 26 ++++++++++-
> formal-model/urcu.spin | 113 ++++++++++++++++++++++-------------------------
> 2 files changed, 77 insertions(+), 62 deletions(-)
>
> diff --git a/formal-model/urcu.sh b/formal-model/urcu.sh
> index b76c764..5e525ec 100644
> --- a/formal-model/urcu.sh
> +++ b/formal-model/urcu.sh
> @@ -1,3 +1,25 @@
> +#!/bin/sh
> +#
> +# Compiles and runs the urcu.spin Promela model.
> +#
> +# This program is free software; you can redistribute it and/or modify
> +# it under the terms of the GNU General Public License as published by
> +# the Free Software Foundation; either version 2 of the License, or
> +# (at your option) any later version.
> +#
> +# This program is distributed in the hope that it will be useful,
> +# but WITHOUT ANY WARRANTY; without even the implied warranty of
> +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
> +# GNU General Public License for more details.
> +#
> +# You should have received a copy of the GNU General Public License
> +# along with this program; if not, write to the Free Software
> +# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
> +#
> +# Copyright (C) IBM Corporation, 2009
> +#
> +# Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> +
> spin -a urcu.spin
> -cc -DSAFETY -o pan pan.c
> -./pan
> +cc -o pan pan.c
> +./pan -a
> diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
> index 3e18457..cf1f670 100644
> --- a/formal-model/urcu.spin
> +++ b/formal-model/urcu.spin
> @@ -40,21 +40,28 @@ bit updater_done = 0;
> byte urcu_gp_ctr = 1;
> byte urcu_active_readers = 0;
>
> +/* must be at least the number of smp_mb() statements in urcu_updater(). */
> +#define N_SMP_MB 9
> +
> /* Model the RCU read-side critical section. */
>
> proctype urcu_reader()
> {
> bit done = 0;
> + byte i;
> bit mbok;
> byte tmp;
> byte tmp_removed;
> byte tmp_free;
>
> /* Absorb any early requests for memory barriers. */
> + i = 0;
> do
> - :: need_mb == 1 ->
> + :: i < N_SMP_MB && need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
>
> @@ -91,12 +98,17 @@ proctype urcu_reader()
> if
> :: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
> tmp = urcu_gp_ctr;
> + i = 0;
> do
> - :: (reader_progress[1] +
> + :: i < N_SMP_MB &&
> + (reader_progress[1] +
> reader_progress[2] +
> - reader_progress[3] == 0) && need_mb == 1 ->
> + reader_progress[3] == 0) &&
> + need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
> urcu_active_readers = tmp;
> @@ -151,10 +163,13 @@ proctype urcu_reader()
> if
> :: mbok == 1 ->
> /* We get here if mb processing is safe. */
> + i = 0;
> do
> - :: need_mb == 1 ->
> + :: i < N_SMP_MB && need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
> :: else -> skip;
> @@ -169,36 +184,30 @@ proctype urcu_reader()
> :: else -> skip;
> fi
> od;
> +
> + /* Make sure any concurrent grace period was sufficiently long. */
> assert((tmp_free == 0) || (tmp_removed == 1));
>
> /* Reader has completed. */
> reader_done = 1;
> -
> - /* Process any late-arriving memory-barrier requests. */
> - do
> - :: need_mb == 1 ->
> - need_mb = 0;
> - :: !updater_done -> skip;
> - :: 1 -> break;
> - od;
> }
>
> +#define smp_mb() \
> + need_mb = 1; \
> + do \
> + :: !reader_done && need_mb == 1 -> skip; \
> + :: reader_done -> break; \
> + :: need_mb == 0 -> break; \
> + od
> +
> /* Model the RCU update process. */
>
> proctype urcu_updater()
> {
> /* prior synchronize_rcu(), second counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -209,27 +218,15 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* Removal statement, e.g., list_del_rcu(). */
> removed = 1;
>
> /* current synchronize_rcu(), first counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -240,24 +237,12 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* current synchronize_rcu(), second counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -268,11 +253,7 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* free-up step, e.g., kfree(). */
> free = 1;
> @@ -299,3 +280,15 @@ 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;
> +}
> --
> 1.5.2.5
>
--
Mathieu Desnoyers
OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F BA06 3F25 A8FE 3BAE 9A68
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 18:18 [PATCH URCU formal] Add liveness checks to user-level RCU model Mathieu Desnoyers
@ 2009-02-20 19:28 ` Paul E. McKenney
2009-02-20 19:46 ` Mathieu Desnoyers
0 siblings, 1 reply; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-20 19:28 UTC (permalink / raw)
To: Mathieu Desnoyers; +Cc: ltt-dev, bert.wesarg, bob, linux-kernel
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?
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;
-}
^ permalink raw reply related [flat|nested] 9+ messages in thread
* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 19:28 ` Paul E. McKenney
@ 2009-02-20 19:46 ` Mathieu Desnoyers
2009-02-20 19:53 ` [ltt-dev] " Mathieu Desnoyers
2009-02-20 20:09 ` Paul E. McKenney
0 siblings, 2 replies; 9+ messages in thread
From: Mathieu Desnoyers @ 2009-02-20 19:46 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: ltt-dev, bert.wesarg, bob, linux-kernel
* 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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [ltt-dev] [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 19:46 ` Mathieu Desnoyers
@ 2009-02-20 19:53 ` Mathieu Desnoyers
2009-02-20 20:11 ` Paul E. McKenney
2009-02-20 20:09 ` Paul E. McKenney
1 sibling, 1 reply; 9+ messages in thread
From: Mathieu Desnoyers @ 2009-02-20 19:53 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: ltt-dev, linux-kernel, bert.wesarg
* Mathieu Desnoyers (compudj@krystal.dyndns.org) wrote:
> * 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);
urcu_gp_ctr = urcu_gp_ctr ^ RCU_GP_CTR_BIT;
is actually much nicer..
MAthieu
>
> 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
>
> _______________________________________________
> ltt-dev mailing list
> ltt-dev@lists.casi.polymtl.ca
> http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
>
--
Mathieu Desnoyers
OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F BA06 3F25 A8FE 3BAE 9A68
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 19:46 ` Mathieu Desnoyers
2009-02-20 19:53 ` [ltt-dev] " Mathieu Desnoyers
@ 2009-02-20 20:09 ` Paul E. McKenney
2009-02-21 1:18 ` Paul E. McKenney
1 sibling, 1 reply; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-20 20:09 UTC (permalink / raw)
To: Mathieu Desnoyers; +Cc: ltt-dev, bert.wesarg, bob, linux-kernel
On Fri, Feb 20, 2009 at 02:46:21PM -0500, Mathieu Desnoyers wrote:
> * 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.
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! :-)
Thanx, Paul
> 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
> --
> To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at http://vger.kernel.org/majordomo-info.html
> Please read the FAQ at http://www.tux.org/lkml/
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [ltt-dev] [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 19:53 ` [ltt-dev] " Mathieu Desnoyers
@ 2009-02-20 20:11 ` Paul E. McKenney
0 siblings, 0 replies; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-20 20:11 UTC (permalink / raw)
To: Mathieu Desnoyers; +Cc: ltt-dev, linux-kernel, bert.wesarg
On Fri, Feb 20, 2009 at 02:53:45PM -0500, Mathieu Desnoyers wrote:
> * Mathieu Desnoyers (compudj@krystal.dyndns.org) wrote:
> > * 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);
> urcu_gp_ctr = urcu_gp_ctr ^ RCU_GP_CTR_BIT;
>
> is actually much nicer..
Good point -- I was forgetting that Promela supports "^".
Thanx, Paul
> MAthieu
> >
> > 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
> >
> > _______________________________________________
> > ltt-dev mailing list
> > ltt-dev@lists.casi.polymtl.ca
> > http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
> >
>
> --
> Mathieu Desnoyers
> OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F BA06 3F25 A8FE 3BAE 9A68
> --
> To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at http://vger.kernel.org/majordomo-info.html
> Please read the FAQ at http://www.tux.org/lkml/
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 20:09 ` Paul E. McKenney
@ 2009-02-21 1:18 ` Paul E. McKenney
0 siblings, 0 replies; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-21 1:18 UTC (permalink / raw)
To: Mathieu Desnoyers; +Cc: ltt-dev, bert.wesarg, bob, linux-kernel
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH URCU formal] Add liveness checks to user-level RCU model.
2009-02-20 17:39 Paul E. McKenney
@ 2009-02-20 18:44 ` Paul E. McKenney
0 siblings, 0 replies; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-20 18:44 UTC (permalink / raw)
To: ltt-dev; +Cc: compudj, bert.wesarg, bob, linux-kernel
By the way, this model does -not- cover Mathieu's scenario where a very
large number of reading processes continually arrive using an obsolete
value of the urcu_gp_ctr variable. Something about having finite memory
on all the machines I have access to. ;-)
So, here is an informal outline of why forward progress is guaranteed
in this situation:
o We assume that if one CPU makes a change to a shared variable,
all other CPUs see the change in a finite period of time.
[CPUs like the semi-SMP Blackfins will need to make this be the
case in software. If you cannot make this assumption, you cannot
prove that -any- non-trivial SMP algorithm will complete.]
o We assume that any given CPU executes code at a finite rate.
Of course, I would be very interested in hearing of any real
hardware that violates this assumption. ;-)
o We assume that all RCU read-side critical sections complete
in finite time (which can be violated if there are CPU-bound
real-time-priority processes unless you have priority boosting,
a scenario I am excluding -- but if this is a real problem,
we need to add priority boosting).
o Then there must be a finite number of threads that have observed
the old value of urcu_gp_ctr.
o Any subsequent RCU read-side critical sections will use the new
value of urcu_gp_ctr.
o The total time consumed by these threads' RCU read-side critical
sections will then be finite.
o The updater will therefore eventually observe all the threads
that used the old value of urcu_gp_ctr to have exited all of
their RCU read-side critical sections.
So given the three assumptions above, forward progress is guaranteed.
Note that although we don't explicitly assume a finite number of threads,
the finite-CPU-speed assumption makes it difficult to see how the updater
scans the per-thread variables in finite time. ;-)
Thanx, Paul
On Fri, Feb 20, 2009 at 09:39:27AM -0800, Paul E. McKenney 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>
> ---
> formal-model/urcu.sh | 26 ++++++++++-
> formal-model/urcu.spin | 113 ++++++++++++++++++++++-------------------------
> 2 files changed, 77 insertions(+), 62 deletions(-)
>
> diff --git a/formal-model/urcu.sh b/formal-model/urcu.sh
> index b76c764..5e525ec 100644
> --- a/formal-model/urcu.sh
> +++ b/formal-model/urcu.sh
> @@ -1,3 +1,25 @@
> +#!/bin/sh
> +#
> +# Compiles and runs the urcu.spin Promela model.
> +#
> +# This program is free software; you can redistribute it and/or modify
> +# it under the terms of the GNU General Public License as published by
> +# the Free Software Foundation; either version 2 of the License, or
> +# (at your option) any later version.
> +#
> +# This program is distributed in the hope that it will be useful,
> +# but WITHOUT ANY WARRANTY; without even the implied warranty of
> +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
> +# GNU General Public License for more details.
> +#
> +# You should have received a copy of the GNU General Public License
> +# along with this program; if not, write to the Free Software
> +# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
> +#
> +# Copyright (C) IBM Corporation, 2009
> +#
> +# Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> +
> spin -a urcu.spin
> -cc -DSAFETY -o pan pan.c
> -./pan
> +cc -o pan pan.c
> +./pan -a
> diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
> index 3e18457..cf1f670 100644
> --- a/formal-model/urcu.spin
> +++ b/formal-model/urcu.spin
> @@ -40,21 +40,28 @@ bit updater_done = 0;
> byte urcu_gp_ctr = 1;
> byte urcu_active_readers = 0;
>
> +/* must be at least the number of smp_mb() statements in urcu_updater(). */
> +#define N_SMP_MB 9
> +
> /* Model the RCU read-side critical section. */
>
> proctype urcu_reader()
> {
> bit done = 0;
> + byte i;
> bit mbok;
> byte tmp;
> byte tmp_removed;
> byte tmp_free;
>
> /* Absorb any early requests for memory barriers. */
> + i = 0;
> do
> - :: need_mb == 1 ->
> + :: i < N_SMP_MB && need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
>
> @@ -91,12 +98,17 @@ proctype urcu_reader()
> if
> :: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
> tmp = urcu_gp_ctr;
> + i = 0;
> do
> - :: (reader_progress[1] +
> + :: i < N_SMP_MB &&
> + (reader_progress[1] +
> reader_progress[2] +
> - reader_progress[3] == 0) && need_mb == 1 ->
> + reader_progress[3] == 0) &&
> + need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
> urcu_active_readers = tmp;
> @@ -151,10 +163,13 @@ proctype urcu_reader()
> if
> :: mbok == 1 ->
> /* We get here if mb processing is safe. */
> + i = 0;
> do
> - :: need_mb == 1 ->
> + :: i < N_SMP_MB && need_mb == 1 ->
> need_mb = 0;
> - :: !updater_done -> skip;
> + i++;
> + :: i < N_SMP_MB ->
> + i++;
> :: 1 -> break;
> od;
> :: else -> skip;
> @@ -169,36 +184,30 @@ proctype urcu_reader()
> :: else -> skip;
> fi
> od;
> +
> + /* Make sure any concurrent grace period was sufficiently long. */
> assert((tmp_free == 0) || (tmp_removed == 1));
>
> /* Reader has completed. */
> reader_done = 1;
> -
> - /* Process any late-arriving memory-barrier requests. */
> - do
> - :: need_mb == 1 ->
> - need_mb = 0;
> - :: !updater_done -> skip;
> - :: 1 -> break;
> - od;
> }
>
> +#define smp_mb() \
> + need_mb = 1; \
> + do \
> + :: !reader_done && need_mb == 1 -> skip; \
> + :: reader_done -> break; \
> + :: need_mb == 0 -> break; \
> + od
> +
> /* Model the RCU update process. */
>
> proctype urcu_updater()
> {
> /* prior synchronize_rcu(), second counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -209,27 +218,15 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* Removal statement, e.g., list_del_rcu(). */
> removed = 1;
>
> /* current synchronize_rcu(), first counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -240,24 +237,12 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* current synchronize_rcu(), second counter flip. */
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
> do
> :: 1 ->
> if
> @@ -268,11 +253,7 @@ proctype urcu_updater()
> :: else -> break;
> fi;
> od;
> - need_mb = 1;
> - do
> - :: need_mb == 1 -> skip;
> - :: need_mb == 0 -> break;
> - od;
> + smp_mb();
>
> /* free-up step, e.g., kfree(). */
> free = 1;
> @@ -299,3 +280,15 @@ 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;
> +}
> --
> 1.5.2.5
>
^ permalink raw reply [flat|nested] 9+ messages in thread
* [PATCH URCU formal] Add liveness checks to user-level RCU model.
@ 2009-02-20 17:39 Paul E. McKenney
2009-02-20 18:44 ` Paul E. McKenney
0 siblings, 1 reply; 9+ messages in thread
From: Paul E. McKenney @ 2009-02-20 17:39 UTC (permalink / raw)
To: ltt-dev; +Cc: compudj, bert.wesarg, bob, linux-kernel, Paul E. McKenney
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>
---
formal-model/urcu.sh | 26 ++++++++++-
formal-model/urcu.spin | 113 ++++++++++++++++++++++-------------------------
2 files changed, 77 insertions(+), 62 deletions(-)
diff --git a/formal-model/urcu.sh b/formal-model/urcu.sh
index b76c764..5e525ec 100644
--- a/formal-model/urcu.sh
+++ b/formal-model/urcu.sh
@@ -1,3 +1,25 @@
+#!/bin/sh
+#
+# Compiles and runs the urcu.spin Promela model.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+#
+# Copyright (C) IBM Corporation, 2009
+#
+# Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+
spin -a urcu.spin
-cc -DSAFETY -o pan pan.c
-./pan
+cc -o pan pan.c
+./pan -a
diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index 3e18457..cf1f670 100644
--- a/formal-model/urcu.spin
+++ b/formal-model/urcu.spin
@@ -40,21 +40,28 @@ bit updater_done = 0;
byte urcu_gp_ctr = 1;
byte urcu_active_readers = 0;
+/* must be at least the number of smp_mb() statements in urcu_updater(). */
+#define N_SMP_MB 9
+
/* Model the RCU read-side critical section. */
proctype urcu_reader()
{
bit done = 0;
+ byte i;
bit mbok;
byte tmp;
byte tmp_removed;
byte tmp_free;
/* Absorb any early requests for memory barriers. */
+ i = 0;
do
- :: need_mb == 1 ->
+ :: i < N_SMP_MB && need_mb == 1 ->
need_mb = 0;
- :: !updater_done -> skip;
+ i++;
+ :: i < N_SMP_MB ->
+ i++;
:: 1 -> break;
od;
@@ -91,12 +98,17 @@ proctype urcu_reader()
if
:: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
tmp = urcu_gp_ctr;
+ i = 0;
do
- :: (reader_progress[1] +
+ :: i < N_SMP_MB &&
+ (reader_progress[1] +
reader_progress[2] +
- reader_progress[3] == 0) && need_mb == 1 ->
+ reader_progress[3] == 0) &&
+ need_mb == 1 ->
need_mb = 0;
- :: !updater_done -> skip;
+ i++;
+ :: i < N_SMP_MB ->
+ i++;
:: 1 -> break;
od;
urcu_active_readers = tmp;
@@ -151,10 +163,13 @@ proctype urcu_reader()
if
:: mbok == 1 ->
/* We get here if mb processing is safe. */
+ i = 0;
do
- :: need_mb == 1 ->
+ :: i < N_SMP_MB && need_mb == 1 ->
need_mb = 0;
- :: !updater_done -> skip;
+ i++;
+ :: i < N_SMP_MB ->
+ i++;
:: 1 -> break;
od;
:: else -> skip;
@@ -169,36 +184,30 @@ proctype urcu_reader()
:: else -> skip;
fi
od;
+
+ /* Make sure any concurrent grace period was sufficiently long. */
assert((tmp_free == 0) || (tmp_removed == 1));
/* Reader has completed. */
reader_done = 1;
-
- /* Process any late-arriving memory-barrier requests. */
- do
- :: need_mb == 1 ->
- need_mb = 0;
- :: !updater_done -> skip;
- :: 1 -> break;
- od;
}
+#define smp_mb() \
+ need_mb = 1; \
+ do \
+ :: !reader_done && need_mb == 1 -> skip; \
+ :: reader_done -> break; \
+ :: need_mb == 0 -> break; \
+ od
+
/* Model the RCU update process. */
proctype urcu_updater()
{
/* prior synchronize_rcu(), second counter flip. */
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
do
:: 1 ->
if
@@ -209,27 +218,15 @@ proctype urcu_updater()
:: else -> break;
fi;
od;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
/* Removal statement, e.g., list_del_rcu(). */
removed = 1;
/* current synchronize_rcu(), first counter flip. */
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
do
:: 1 ->
if
@@ -240,24 +237,12 @@ proctype urcu_updater()
:: else -> break;
fi;
od;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
/* current synchronize_rcu(), second counter flip. */
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
do
:: 1 ->
if
@@ -268,11 +253,7 @@ proctype urcu_updater()
:: else -> break;
fi;
od;
- need_mb = 1;
- do
- :: need_mb == 1 -> skip;
- :: need_mb == 0 -> break;
- od;
+ smp_mb();
/* free-up step, e.g., kfree(). */
free = 1;
@@ -299,3 +280,15 @@ 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;
+}
--
1.5.2.5
^ permalink raw reply related [flat|nested] 9+ messages in thread
end of thread, other threads:[~2009-02-21 1:19 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-02-20 18:18 [PATCH URCU formal] Add liveness checks to user-level RCU model Mathieu Desnoyers
2009-02-20 19:28 ` Paul E. McKenney
2009-02-20 19:46 ` Mathieu Desnoyers
2009-02-20 19:53 ` [ltt-dev] " Mathieu Desnoyers
2009-02-20 20:11 ` Paul E. McKenney
2009-02-20 20:09 ` Paul E. McKenney
2009-02-21 1:18 ` Paul E. McKenney
-- strict thread matches above, loose matches on Subject: below --
2009-02-20 17:39 Paul E. McKenney
2009-02-20 18:44 ` Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).