[ltt-dev] [PATCH URCU formal] Add liveness checks to user-level RCU model.

[Paul E. McKenney]

On Fri, Feb 20, 2009 at 01:18:35PM -0500, Mathieu Desnoyers wrote:
> * Paul E. McKenney (paulmck at 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 at 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 at 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 at 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;
-}