code review 75130045: doc: allow buffered channel as semaphore without initia...

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.

[rsc, 2014-03-13 03:05:02]

Hello golang-codereviews@googlegroups.com,

I'd like you to review this change to
https://code.google.com/p/go/

[rsc, 2014-03-13 03:29:37]

R=r
but i want dvyukov's review too

[r, 2014-03-13 03:32:03]

LGTM

[r, 2014-03-13 03:32:38]

(by the way, Effective Go does say this, informally, so it is written down.)

[Dominik Honnef, 2014-03-13 03:34:13]

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?

[r, 2014-03-13 05:02:49]

NOT LGTM

I've changed my mind. This makes things more confusing not less. Compare and
contrast with Effecctive Go.

[r, 2014-03-13 05:03:17]

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

[dvyukov, 2014-03-13 09:07:56]

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.

[dvyukov, 2014-03-13 09:09:36]

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.

[kortschak, 2014-03-13 10:54:40]

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.

[r, 2014-03-13 11:18:20]

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

[dvyukov, 2014-03-13 11:52:48]

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

[rsc, 2014-03-13 13:31:28]

It contradicts Effective Go because you changed effective Go under duress
last March.
https://codereview.appspot.com/7698045/diff/14001/doc/effective_go.html

[rsc, 2014-03-13 14:20:41]

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

[rsc, 2014-03-13 15:15:07]

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

[r, 2014-03-13 20:50:54]

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.

[rsc, 2014-03-13 20:51:32]

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.

[kortschak, 2014-03-13 20:59:48]

LGTM

Thank you for this.

[iant, 2014-03-13 22:03:09]

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#newc...
doc/effective_go.html:2951: var sem = make(chan int, MaxOutstanding)
Since the values are irrelevant, should we consider changing this to chan bool?

[dvyukov, 2014-03-14 05:59:53]

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

[dvyukov, 2014-03-14 06:10:15]

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.

[0xjnml, 2014-03-20 10:34:58]

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.

[rsc, 2014-03-24 23:11:26]

*** 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.