On Sat, Apr 14, 2018 at 7:02 PM Penguin Enormous <kimkhanh...@gmail.com> wrote:
> 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.
