Code review - Issue 75130045: code review 75130045: doc: allow buffered channel as semaphore without initia...https://codereview.appspot.com/2014-03-24T23:11:26+00:00rietveld
Message from unknown
2014-03-13T03:04:52+00:00rscurn:md5:8ad8db420f7483455ab1e651ac287e46
Message from unknown
2014-03-13T03:04:55+00:00rscurn:md5:a30e0c572d5818aa177d186fe8cd18a6
Message from unknown
2014-03-13T03:04:58+00:00rscurn:md5:3967e59be0c93633887fbbf5bf6c2c74
Message from rsc@golang.org
2014-03-13T03:05:02+00:00rscurn:md5:61094b4a67c8e81e76a63e5eaf56865c
Hello golang-codereviews@googlegroups.com,
I'd like you to review this change to
https://code.google.com/p/go/
Message from rsc@golang.org
2014-03-13T03:29:37+00:00rscurn:md5:8a29c5a4092c0ee227739fc44a1c978e
R=r
but i want dvyukov's review too
Message from r@golang.org
2014-03-13T03:32:03+00:00rurn:md5:fddb14fa1218e091b898ffc41c54675a
LGTM
Message from r@golang.org
2014-03-13T03:32:38+00:00rurn:md5:e822bcfa1127144dee7e46496d520181
(by the way, Effective Go does say this, informally, so it is written down.)
Message from dominik.honnef@gmail.com
2014-03-13T03:34:13+00:00Dominik Honnefurn:md5:740a37b94469d932f3477070272d7805
On 2014/03/13 03:32:38, r wrote:
> (by the way, Effective Go does say this, informally, so it is written down.)
Doesn't Effective Go currently say that acquire needs to be a receive, not a send, and thus requires to fill the channel first?
Message from r@golang.org
2014-03-13T05:02:49+00:00rurn:md5:1e73b66dc57b5558e174f0dd6b099b9a
NOT LGTM
I've changed my mind. This makes things more confusing not less. Compare and contrast with Effecctive Go.
Message from r@golang.org
2014-03-13T05:03:17+00:00rurn:md5:f72c395032ad7df402ea9dcbb2f83ccc
OK, now I am once again confused. It's not the first time and it won't
be the last.
Here's what Effective Go says:
Because data synchronization occurs on a receive from a channel
(that is, the send "happens before" the receive; see
<a href="/ref/mem">The Go Memory Model</a>),
acquisition of the semaphore must be on a channel receive, not a send.
If you look very carefully, you'll see that this is not in
contradiction to the phrase
sending an item acquires the semaphore, and receiving an item releases
the semaphore
because things are inside out and backwards but if this CL is supposed
to support what's in EG rather than appear to contradict it, it's
failing.
-rob
Message from dvyukov@google.com
2014-03-13T09:07:56+00:00dvyukovurn:md5:4f567fe435283b92c417f824e7d2d5c2
I find this "inverted" semaphore a bit confusing. Probably I would not add the similar for sync channels in the first place, sending satellite data by means of a receive operation is confusing and rarely useful (I understand that we can't remove it now, though).
But what I am after is that we need to make the rules consistent between the spec and the memory model (and the race detector). If we agree that the inverted buffered-chan-based semaphore is legal for rate limiting, then this must be reflected in MM as well. Because MM is the foundation for reasoning about concurrent activities. For me "there is no more than N of X at the same time" is equivalent to "there is no more than N unordered X in the happens-before graph". Such formal definition makes it easy/possible to prove or disprove various properties. I am against making distinction between "memory" and "non-memory" operations, because in the end it's very vague, and otherwise there would be no foundation for reasoning about concurrent "non-memory" operations.
Message from dvyukov@google.com
2014-03-13T09:09:36+00:00dvyukovurn:md5:65f916db2d71b08500d30374d8a2801e
On 2014/03/13 09:07:56, dvyukov wrote:
> I find this "inverted" semaphore a bit confusing. Probably I would not add the
> similar for sync channels in the first place, sending satellite data by means of
> a receive operation is confusing and rarely useful (I understand that we can't
> remove it now, though).
>
> But what I am after is that we need to make the rules consistent between the
> spec and the memory model (and the race detector). If we agree that the inverted
> buffered-chan-based semaphore is legal for rate limiting, then this must be
> reflected in MM as well. Because MM is the foundation for reasoning about
> concurrent activities. For me "there is no more than N of X at the same time" is
> equivalent to "there is no more than N unordered X in the happens-before graph".
> Such formal definition makes it easy/possible to prove or disprove various
> properties. I am against making distinction between "memory" and "non-memory"
> operations, because in the end it's very vague, and otherwise there would be no
> foundation for reasoning about concurrent "non-memory" operations.
To make it clear, this change to MM satisfies the properties that I am talking about.
Message from dan.kortschak@adelaide.edu.au
2014-03-13T10:54:40+00:00kortschakurn:md5:f7bc3dd0b2ec3e3263a1b205e677aa9b
That is due to the fact that Effective Go was changed in 1a329995118c because of Issue 5023, the very issue being dealt with hear but in the opposite direction. Contradiction is to be expected.
Message from r@golang.org
2014-03-13T11:18:20+00:00rurn:md5:59a4bdd240a31485919eae3ed210b04a
My take: without careful study and reasoning, this example seems to
contradict the claims in Effective Go, so either that document has to
be updated to explain why this inversion works, or this one should
contain both the forward and backwards semaphore models.
I'm not the smartest guy here, far from it, but I believe I should be
able to understand this. I can, but not without staring at the
examples very hard.
-rob
Message from dvyukov@google.com
2014-03-13T11:52:48+00:00dvyukovurn:md5:61ba63c966d75f63c7c9e8b7fffd3e44
On Thu, Mar 13, 2014 at 3:17 PM, Rob Pike <r@golang.org> wrote:
> My take: without careful study and reasoning, this example seems to
> contradict the claims in Effective Go, so either that document has to
> be updated to explain why this inversion works, or this one should
> contain both the forward and backwards semaphore models.
I think this change also needs to update Effective Go (revert back to
inverted semaphore as it was originally). And as an explanation that
example in Effective Go can now refer to the Memory Model (which
contains a similar example and explains why it works).
> I'm not the smartest guy here, far from it, but I believe I should be
> able to understand this. I can, but not without staring at the
> examples very hard.
>
> -rob
Message from rsc@golang.org
2014-03-13T13:31:28+00:00rscurn:md5:82fc7389d1f155ba1163fe8f9a40b1ee
It contradicts Effective Go because you changed effective Go under duress
last March.
https://codereview.appspot.com/7698045/diff/14001/doc/effective_go.html
Message from unknown
2014-03-13T14:19:05+00:00rscurn:md5:57f96933090f4725959df86949ad33a0
Message from rsc@golang.org
2014-03-13T14:20:41+00:00rscurn:md5:1f722fac07b0b5ba9ec00d3179b9ade4
I have added effective_go.html to this CL. I replaced the Go 1.1 example
with the original example and adjusted the text accordingly.
I think the complexity here is primarily in the history of the discussions.
We've always intended this to work, as evidenced by its use in Effective Go
from the start.
Russ
Message from rsc@golang.org
2014-03-13T15:15:07+00:00rscurn:md5:17aaa55c50a04fc1a3a23bc641af2895
My view of the history follows.
Certainly Rob and I have always expected the counting semaphore example in
this CL to work. It was Rob's first complete
draft<https://code.google.com/p/go/source/detail?r=339fa3f7219a>of the
concurrency section, which I reviewed (before Go was open sourced).
People have objected to this example on the grounds that it is not
justified by the memory model. Those objections got loud enough last year
that Rob rewrote the example (CL
7698045<https://codereview.appspot.com/7698045/diff/14001/doc/effective_go.html>).
They started again when I used the original form in a rate limiter in
package net (CL 13038043 <https://codereview.appspot.com/13038043>).
My position is that any use of the original form as a counting semaphore
with capacity C > 1 needs no justification using the memory model at all.
It follows from the definition of buffered channels that C+1 sends cannot
happen until at least 1 receive has happened. The memory model is about
steps a program can take to guarantee that goroutines see a consistent view
of *memory*, which is a much narrower scope. The counting semaphore example
allows C goroutines to execute some critical section simultaneously: if C >
1, the goroutines must find another way to coordinate access to any shared
memory, no matter what the memory model says.
With capacity C = 1, the example becomes a simple mutex, and then you might
want the memory model to make some guarantees, so that you can use the
channel mutex to coordinate access to memory.
The general rule being added in this CL reduces to the existing unbuffered
rule when C = 0, and it guarantees the correct execution of code using a
channel mutex when C = 1. I believe the C > 1 case needs no guarantee, but
others disagree with me, and I believe it is not harmful to future
implementations to make the guarantee. Writing the general rule is cleaner
than writing a rule for just C = 0 and C = 1, and it should end the debate
over C > 1.
Russ
Message from r@golang.org
2014-03-13T20:50:54+00:00rurn:md5:cedd089e728918713d290e56de3ddae9
LGTM but wait for dvyukov
The story is that the memory model now supports the way we want this example to work, without requiring pre-loading the buffered channel. The previous version of the semaphore is still correct, just unnecessarily complicated and somewhat weird in its justification.
Message from rsc@golang.org
2014-03-13T20:51:32+00:00rscurn:md5:280e9bf66221a412cefdfb5898de015a
Dmitriy, I had a hard time understanding your responses.
Do you agree that the CL makes the init-free idiom legal?
Are you in favor of the CL?
Thanks.
Message from dan.kortschak@adelaide.edu.au
2014-03-13T20:59:48+00:00kortschakurn:md5:0c6ea5df61df306389898f6f497c4988
LGTM
Thank you for this.
Message from iant@golang.org
2014-03-13T22:03:09+00:00ianturn:md5:2a2f688143669b3fbc0a2d61827f06af
LGTM
https://codereview.appspot.com/75130045/diff/60001/doc/effective_go.html
File doc/effective_go.html (right):
https://codereview.appspot.com/75130045/diff/60001/doc/effective_go.html#newcode2951
doc/effective_go.html:2951: var sem = make(chan int, MaxOutstanding)
Since the values are irrelevant, should we consider changing this to chan bool?
Message from dvyukov@google.com
2014-03-14T05:59:53+00:00dvyukovurn:md5:8863fa5f54cb4c2b52e6ad9de881e8f7
On 2014/03/13 20:51:32, rsc wrote:
> Dmitriy, I had a hard time understanding your responses.
>
> Do you agree that the CL makes the init-free idiom legal?
Yes.
> Are you in favor of the CL?
LGTM
Message from dvyukov@google.com
2014-03-14T06:10:15+00:00dvyukovurn:md5:d83176a8431941e82acdb738046c98ba
On 2014/03/13 15:15:07, rsc wrote:
> My view of the history follows.
>
> Certainly Rob and I have always expected the counting semaphore example in
> this CL to work. It was Rob's first complete
> draft<https://code.google.com/p/go/source/detail?r=339fa3f7219a>of the
> concurrency section, which I reviewed (before Go was open sourced).
>
> People have objected to this example on the grounds that it is not
> justified by the memory model. Those objections got loud enough last year
> that Rob rewrote the example (CL
> 7698045<https://codereview.appspot.com/7698045/diff/14001/doc/effective_go.html>).
> They started again when I used the original form in a rate limiter in
> package net (CL 13038043 <https://codereview.appspot.com/13038043>).
>
> My position is that any use of the original form as a counting semaphore
> with capacity C > 1 needs no justification using the memory model at all.
> It follows from the definition of buffered channels that C+1 sends cannot
> happen until at least 1 receive has happened. The memory model is about
> steps a program can take to guarantee that goroutines see a consistent view
> of *memory*, which is a much narrower scope. The counting semaphore example
> allows C goroutines to execute some critical section simultaneously: if C >
> 1, the goroutines must find another way to coordinate access to any shared
> memory, no matter what the memory model says.
>
> With capacity C = 1, the example becomes a simple mutex, and then you might
> want the memory model to make some guarantees, so that you can use the
> channel mutex to coordinate access to memory.
>
> The general rule being added in this CL reduces to the existing unbuffered
> rule when C = 0, and it guarantees the correct execution of code using a
> channel mutex when C = 1. I believe the C > 1 case needs no guarantee, but
> others disagree with me, and I believe it is not harmful to future
> implementations to make the guarantee.
Agree.
For round-robin-buffer-based implementation (like what we have now), this guarantee is automatically ensured by the fact that chan implementation needs to synchronize accesses to elements of the buffer (before writing data send must ensure that the previous receive has indeed completed).
This guarantee is also always hold for any mutex-protected implementation.
It's possible to imagine a lock-free linked-list-based implementation, where this guarantee does not automatically hold; but (1) we need/want it for C=1 case, (2) probably the impl could skip the additional memory barriers for C>1 case, (3) lock-free linked-list queues are slow anyway.
> Writing the general rule is cleaner
> than writing a rule for just C = 0 and C = 1, and it should end the debate
> over C > 1.
Message from 0xjnml@gmail.com
2014-03-20T10:34:58+00:000xjnmlurn:md5:3dc47a536277dc1484ccf39fe68a8b1d
https://codereview.appspot.com/75130045/diff/60001/doc/go_mem.html
File doc/go_mem.html (right):
https://codereview.appspot.com/75130045/diff/60001/doc/go_mem.html#newcode303
doc/go_mem.html:303: limit <- 1
I think the send should be before the above go statement. I see that the mechanism works in the current version. It's only not scaling well for big amount of work - a lot of (memory consuming) goroutines are created when only some of them can make progress. Moving the send before the go statement avoids that.
Message from unknown
2014-03-24T23:11:17+00:00rscurn:md5:f5dfd4c4af777a5f3aeb4c5244ab249b
Message from rsc@golang.org
2014-03-24T23:11:26+00:00rscurn:md5:c78e83f1c3b08a31b4d5a9437da31985
*** Submitted as https://code.google.com/p/go/source/detail?r=8e4393a5626f ***
doc: allow buffered channel as semaphore without initialization
This rule not existing has been the source of many discussions
on golang-dev and on issues. We have stated publicly that it is
true, but we have never written it down. Write it down.
Fixes issue 6242.
LGTM=r, dan.kortschak, iant, dvyukov
R=golang-codereviews, r, dominik.honnef, dvyukov, dan.kortschak, iant, 0xjnml
CC=golang-codereviews
https://codereview.appspot.com/75130045
https://codereview.appspot.com/75130045/diff/60001/doc/go_mem.html
File doc/go_mem.html (right):
https://codereview.appspot.com/75130045/diff/60001/doc/go_mem.html#newcode303
doc/go_mem.html:303: limit <- 1
On 2014/03/20 10:34:58, 0xjnml wrote:
> I think the send should be before the above go statement. I see that the
> mechanism works in the current version. It's only not scaling well for big
> amount of work - a lot of (memory consuming) goroutines are created when only
> some of them can make progress. Moving the send before the go statement avoids
> that.
thanks but no thanks. that's getting to be a distraction from the main point.