Messages in this thread Patch in this message | | | Date | Fri, 20 Feb 2009 11:28:24 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH URCU formal] Add liveness checks to user-level RCU model. |
| |
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; -}
| |