On Thu, Feb 12, 2009 at 12:47:07AM -0500, Mathieu Desnoyers wrote:
quoted text
> * Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote:
> > On Wed, Feb 11, 2009 at 11:10:44PM -0500, Mathieu Desnoyers wrote:
> > > * Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote:
> > > > On Wed, Feb 11, 2009 at 06:33:08PM -0800, Paul E. McKenney wrote:
> > > > > On Wed, Feb 11, 2009 at 04:35:49PM -0800, Paul E. McKenney wrote:
> > > > > > On Wed, Feb 11, 2009 at 04:42:58PM -0500, Mathieu Desnoyers wrote:
> > > > > > > * Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote:
> > > > 
> > > > [ . . . ]
> > > > 
> > > > > > > > (BTW, I do not trust my model yet, as it currently cannot detect the
> > > > > > > > failure case I pointed out earlier.  :-/  Here and I thought that the
> > > > > > > > point of such models was to detect additional failure cases!!!)
> > > > > > > > 
> > > > > > > 
> > > > > > > Yes, I'll have to dig deeper into it.
> > > > > > 
> > > > > > Well, as I said, I attached the current model and the error trail.
> > > > > 
> > > > > And I had bugs in my model that allowed the rcu_read_lock() model
> > > > > to nest indefinitely, which overflowed into the top bit, messing
> > > > > things up.  :-/
> > > > > 
> > > > > Attached is a fixed model.  This model validates correctly (woo-hoo!).
> > > > > Even better, gives the expected error if you comment out line 180 and
> > > > > uncomment line 213, this latter corresponding to the error case I called
> > > > > out a few days ago.
> > > > > 
> > > > > I will play with removing models of mb...
> > > > 
> > > > And commenting out the models of mb between the counter flips and the
> > > > test for readers still passes validation, as expected, and as shown in
> > > > the attached Promela code.
> > > > 
> > > 
> > > Hrm, in the email I sent you about the memory barrier, I said that it
> > > would not make the algorithm incorrect, but that it would cause
> > > situations where it would be impossible for the writer to do any
> > > progress as long as there are readers active. I think we would have to
> > > enhance the model or at least express this through some LTL statement to
> > > validate this specific behavior.
> > 
> > But if the writer fails to make progress, then the counter remains at a
> > given value, which causes readers to drain, which allows the writer to
> > eventually make progress again.  Right?
> > 
> 
> Not necessarily. If we don't have the proper memory barriers, we can
> have the writer waiting on, say, parity 0 *before* it has performed the
> parity switch. Therefore, even newly coming readers will add up to
> parity 0.

But the write that changes the parity will eventually make it out.
OK, so your argument is that we at least need a compiler barrier?

Regardless, please see attached for a modified version of the Promela
model that fully models omitting out the memory barrier that my
rcu_nest32.[hc] implementation omits.  (It is possible to partially
model removal of other memory barriers via #if 0, but to fully model
would need to enumerate the permutations as shown on lines 231-257.)

quoted text
> In your model, this is not detected, because eventually all readers will
> execute, and only then the writer will be able to update the data. But
> in reality, if we run a very busy 4096-cores machines where there is
> always at least one reader active, the the writer will be stuck forever,
> and that's really bad.

Assuming that the reordering is done by the CPU, the write will
eventually get out -- it is stuck in (say) the store buffer, and the
cache line will eventually arrive, and then the value will eventually
be seen by the readers.

We might need a -compiler- barrier, but then again, I am not sure that
we are talking about the same memory barrier -- again, please see
attached lines 231-257 to see which one that I eliminated.

Also, the original model I sent out has a minor bug that prevents it
from fully modeling the nested-read-side case.  The patch below fixes this.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---

 urcu.spin |    6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index e5bfff3..611464b 100644
--- a/formal-model/urcu.spin
+++ b/formal-model/urcu.spin
@@ -124,9 +124,13 @@ proctype urcu_reader()
 				break;
 			:: tmp < 4 && reader_progress[tmp] != 0 ->
 				tmp = tmp + 1;
-			:: tmp >= 4 ->
+			:: tmp >= 4 &&
+			   reader_progress[0] == reader_progress[3] ->
 				done = 1;
 				break;
+			:: tmp >= 4 &&
+			   reader_progress[0] != reader_progress[3] ->
+			   	break;
 			od;
 			do
 			:: tmp < 4 && reader_progress[tmp] == 0 ->