On Sat, Apr 14, 2018 at 7:02 PM Penguin Enormous <kimkhanh...@gmail.com>

> But looking at your answer, I see that you may imply certain race
> conditions are allowed. Could you explain a bit more on that? Aren't race
> conditions supposedly bad?
Race conditions can, in certain cases, be benign if guarded properly by
some other code. As long as you eventually solve the race in a valid way.
This is of course somewhat brittle, so the usual recommendation is to avoid
these. However, in low-level runtime code inside a system, you can use
these quasi-races to speed up the code in certain situations.

In your example, we have another possible ordering which your code must
handle as well: suppose the atomic.Xadd(&l.wait, 1) happens *after* the
signaler runs line 522. In this case, you are also blocked forever until we
signal again.

I think that if you want to prove the current model works, you need to take
sync.Cond.L (Locker) into account as well. The functions you mention
requires you to hold L on the waiter side when calling Wait(), and the
signaler needs to hold L as well at some point, though not necessarily when
calling Signal(). This is probably crucial in a proof of correctness on the
concurrency of said routine. Another important point is the relationship
between wait and notify, and the fact that each wait ticket is unique. This
establishes a kind of lemma on the ordering of wait and notify. Something
you can probably exploit in your full proof. Or to be more precise: it is
crucial you load wait before notify and the check for equality can only
happen if the routine "caught up". Also, your proof must hold if you remove
the fast-path check in line 522.

You received this message because you are subscribed to the Google Groups 
"golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to golang-nuts+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to