That sounds like a nice property. I'd suggest the wording:
"A receive from a buffered channel that is full happens before the
send on that channel completes."
> If this relationship wouldn't hold, one could imaging multiple goroutines
> sending to a channel beyond its capacity.
That's a different statement. We can say the channel blocks while full
without offering all the guarantees of happens-before. We've just had
a long thread about this without reaching consensus, though, so I
suggest simply avoiding getting into this topic again. We can try to
reach agreement on the prior changes without this.
Actually, I take that back. I can't see why this property would be
beneficial. It would mean having to memory fences between sends and
completely unrelated receives.
I'm personally happy with the current wording in the memory model.
We could also implement a semaphore without the subtlety of whether we first fill it up or not.
Communicate by using channels, and use a real lock if you really want
to share memory.
I'd prefer to have a proper semaphore in sync instead of abusing
channels for that.
In a previous post ( https://groups.google.com/d/msg/golang-nuts/qt3ABSpKjzM/c9uLkKLZ05QJ ), Rog pointed out that he hadn't seen any convincing argument that would guarantee that the following program doesn't panic:Go's memory model for channel communications only states 3 "happens before" cases:1) "A send on a channel happens before the corresponding receive from
that channel completes."
2) "The closing of a channel happens before a receive that returns a
zero value because the channel is closed."
3) "A receive from an unbuffered channel happens before the send on that
channel completes."My understanding is that buffered channels also need a "happens before" relationship along the following lines:4) "A receive from an full channel happens before the send on that
channel completes."If this relationship wouldn't hold, one could imaging multiple goroutines sending to a channel beyond its capacity.
Note also that case 4) would also ensure that Rog's program doesn't panic.Does the document "Go's memory model" need amendment?
If this relationship wouldn't hold, one could imaging multiple goroutines sending to a channel beyond its capacity.The chan itself is always consistent (i.e. max capacity is respected), but it does not mean that the operations synchronize any auxiliary data.
To be clear, I still believe that case 4) holds implicitly, but people shouldn't rely on it for synchronising data.
On Saturday, May 25, 2013 2:26:15 PM UTC+1, Dmitry Vyukov wrote:If this relationship wouldn't hold, one could imaging multiple goroutines sending to a channel beyond its capacity.The chan itself is always consistent (i.e. max capacity is respected), but it does not mean that the operations synchronize any auxiliary data.I didn't want to question that.What I meant is that as a consequence of chan itself been consistent, one could also conclude that sends from any goroutine cannot happen while a chan is full.
This, if my reasoning is not flawed, is equivalent to saying goroutines are bound by a "happens before" relationship with the receive that stops that channel from being full.That's why I proposed adding a 4th case to go's memory model document.
But now, I feel my position it's closer to Gustavo's side, and I think people should be discouraged from using channels to synchronise any other data than that going through the channel itself.
To be clear, I still believe that case 4) holds implicitly, but people shouldn't rely on it for synchronising data.
--
To be clear, I still believe that case 4) holds implicitly, but people shouldn't rely on it for synchronising data.I don't understand how something can be true, but not sufficiently true enough to be relied upon.
Yes, sends cannot happen while a chan is full. But this does not establish happens-before. Happens-before relation is transitive and so it orders other operations. This "sends cannot happen while a chan is full" is not transitive, it does not affect any other operations.
> Are you sure you want this code to be legal?
Personally, I would, yes.
I think it's as reasonable for a close operation to be "before"
another close operation that panics because of the previous one.
I might be the only one that thinks so at this point, though.
The chan itself is always consistent (i.e. max capacity is respected), but it does not mean that the operations synchronize any auxiliary data.If you are familiar with C/C++ memory model, the analog of the operations is:void send(struct chan *c) {int sz = atomic_load_explicit(&c->sz, memory_order_relaxed);for(;;) {if(sz == c->cap)continue;if(atomic_compare_exchange_weak_explicit(&c->sz, &sz, sz+1, memory_order_release))break;
}
}
On Sunday, May 26, 2013 9:01:00 AM UTC+1, Dmitry Vyukov wrote:Yes, sends cannot happen while a chan is full. But this does not establish happens-before. Happens-before relation is transitive and so it orders other operations. This "sends cannot happen while a chan is full" is not transitive, it does not affect any other operations.It does affect all the operations after the send that was initially blocked.
Gustavo mentioned that in the "Effective Go" tutorial, the implementation of a semaphore was changed so that synchronisation only relied on channel receives. Here's a question: was this change prompted because the implementation was actually found to fail or because it couldn't be proved using the document "Go's memory model"?Because what I'm arguing is that any go implementation that stops a buffered channel from overloading is implicitly also doing a synchronisation as described in case 4).Is it possible to come up with an example using buffered channels where case 4) doesn't hold? That would prove my reasoning is flawed somehow.
NicoPS: I'll go through the rest of your email later.
--
--
On Mon, May 27, 2013 at 10:26 AM, Dmitry Vyukov <dvy...@google.com> wrote:Agreed, but as long as it doesn't break the specification, which
> Yes, it is.
> The simplest thing is just to execute some operations, that are after the
> send in program order, before the send.
implies that sends block if the channel is full.
In other words, doing
ch <- v
s, err := l.Accept()
As
s, err := l.Accept()
ch <- v
Is breaking the specification, and is also nuts if we expect people to
know what their programs do.
void send(struct chan *c) {int sz = atomic_load_explicit(&c->sz, memory_order_relaxed);for(;;) {if(sz == c->cap)continue;if(atomic_compare_exchange_weak_explicit(&c->sz, &sz, sz+1, memory_order_release))break;
}
}
On Mon, May 27, 2013 at 3:55 PM, Nico <nicolas...@gmail.com> wrote:I'm trying to understand the code above.If sz equals c->cap, send(c) seems to enter a infinite loop because sz and c->cap don't get updated before iterating again.Shouldn't sz get updated before iterating again, as it happens in the atomic_compare_exchange_weak()?
On Monday, May 27, 2013 9:27:52 AM UTC-4, Dmitry Vyukov wrote:atomic_compare_exchange_weak_explicit() updates comparand on failure.
sz is thread local. c->Cap is constant. some form of non-local non-constant read inside the loop before the continue statement,or you have an infinite loop. you are either missing a line, or that first line is really supposed to be inside the loop.