code review 101330056: doc: ban data races (issue 101330056 by dvyukov@google.com)

[dvy...@google.com]

Reviewers: golang-codereviews,

Message:
Hello golang-co...@googlegroups.com (cc: k...@golang.org,
r...@golang.org, r...@golang.org),

I'd like you to review this change to
https://dvyukov%40goog...@code.google.com/p/go/


Description:
doc: ban data races
The current wording tries to give at least some guarantees
to programs with data races.
This is (1) not very useful, as races on primitive types can be easily
fixed using sync/atomic package, (2) most likely is not implemented,
in particular in gccgo which I believe assumes race-free programs,
(3) can inhibit useful optimizations in future (e.g. code generation
optimizations or concurrent garbage collection).
I believe this classifies as "bug fix" with respect to Go1 promise.

Please review this at https://codereview.appspot.com/101330056/

Affected files (+14, -71 lines):
M doc/go_mem.html


Index: doc/go_mem.html
===================================================================
--- a/doc/go_mem.html
+++ b/doc/go_mem.html
@@ -24,20 +24,6 @@
<h2>Happens Before</h2>

<p>
-Within a single goroutine, reads and writes must behave
-as if they executed in the order specified by the program.
-That is, compilers and processors may reorder the reads and writes
-executed within a single goroutine only when the reordering
-does not change the behavior within that goroutine
-as defined by the language specification.
-Because of this reordering, the execution order observed
-by one goroutine may differ from the order perceived
-by another. For example, if one goroutine
-executes <code>a = 1; b = 2;</code>, another might observe
-the updated value of <code>b</code> before the updated value of
<code>a</code>.
-</p>
-
-<p>
To specify the requirements of reads and writes, we define
<i>happens before</i>, a partial order on the execution
of memory operations in a Go program. If event <span
class="event">e₁</span> happens
@@ -52,39 +38,35 @@
</p>

<p>
-A read <span class="event">r</span> of a variable <code>v</code> is
<i>allowed</i> to observe a write <span class="event">w</span> to
<code>v</code>
+A read <span class="event">r</span> of a variable <code>v</code> observes
a write <span class="event">w</span> to <code>v</code>
if both of the following hold:
</p>

<ol>
-<li><span class="event">r</span> does not happen before <span
class="event">w</span>.</li>
-<li>There is no other write <span class="event">w'</span> to
<code>v</code> that happens
- after <span class="event">w</span> but before <span
class="event">r</span>.</li>
+<li><span class="event">w</span> happens before <span
class="event">r</span>.</li>
+<li>There is no other write <span class="event">w'</span> to <code>v</code>
+such that <span class="event">w</span> happens before <span
class="event">w'</span>
+and <span class="event">w'</span> happens before <span
class="event">r</span>.</li>
</ol>

<p>
-To guarantee that a read <span class="event">r</span> of a variable
<code>v</code> observes a
-particular write <span class="event">w</span> to <code>v</code>, ensure
that <span class="event">w</span> is the only
-write <span class="event">r</span> is allowed to observe.
-That is, <span class="event">r</span> is <i>guaranteed</i> to observe
<span class="event">w</span> if both of the following hold:
+The execution of a program contains <i>a data race</i> if it contains
+two memory accesses to the same shared variable in different goroutines
such that:
</p>

<ol>
-<li><span class="event">w</span> happens before <span
class="event">r</span>.</li>
-<li>Any other write to the shared variable <code>v</code>
-either happens before <span class="event">w</span> or after <span
class="event">r</span>.</li>
+<li>At least one of the memory accesses is a write.</li>
+<li>The memory accesses happen concurrently.</li>
</ol>

<p>
-This pair of conditions is stronger than the first pair;
-it requires that there are no other writes happening
-concurrently with <span class="event">w</span> or <span
class="event">r</span>.
+Any such data race results in <i>undefined behavior</i>.
</p>

<p>
Within a single goroutine,
-there is no concurrency, so the two definitions are equivalent:
-a read <span class="event">r</span> observes the value written by the most
recent write <span class="event">w</span> to <code>v</code>.
+there is no concurrency, so a read <span class="event">r</span> observes
the value
+written by the most recent write <span class="event">w</span> to
<code>v</code>.
When multiple goroutines access a shared variable <code>v</code>,
they must use synchronization events to establish
happens-before conditions that ensure reads observe the
@@ -96,12 +78,6 @@
for <code>v</code>'s type behaves as a write in the memory model.
</p>

-<p>
-Reads and writes of values larger than a single machine word
-behave as multiple machine-word-sized operations in an
-unspecified order.
-</p>
-
<h2>Synchronization</h2>

<h3>Initialization</h3>
@@ -318,7 +294,7 @@

<p class="rule">
For any <code>sync.Mutex</code> or <code>sync.RWMutex</code> variable
<code>l</code> and <i>n</i> &lt; <i>m</i>,
-call <i>n</i> of <code>l.Unlock()</code> happens before call <i>m</i> of
<code>l.Lock()</code> returns.
+call <i>n</i> of <code>l.Unlock()</code> happens before call <i>m</i> of
<code>l.Lock()</code>.
</p>

<p>
@@ -402,40 +378,7 @@
<h2>Incorrect synchronization</h2>

<p>
-Note that a read <span class="event">r</span> may observe the value
written by a write <span class="event">w</span>
-that happens concurrently with <span class="event">r</span>.
-Even if this occurs, it does not imply that reads happening after <span
class="event">r</span>
-will observe writes that happened before <span class="event">w</span>.
-</p>
-
-<p>
-In this program:
-</p>
-
-<pre>
-var a, b int
-
-func f() {
- a = 1
- b = 2
-}
-
-func g() {
- print(b)
- print(a)
-}
-
-func main() {
- go f()
- g()
-}
-</pre>
-
-<p>
-it can happen that <code>g</code> prints <code>2</code> and then
<code>0</code>.
-</p>
-
-<p>
+Go does not define behavior of programs with data races.
This fact invalidates a few common idioms.
</p>

[da...@cheney.net]

I agree with these points, I think this should land (I'm deliberately
avoid those four consonants)

https://codereview.appspot.com/101330056/

[ia...@golang.org]

https://codereview.appspot.com/101330056/diff/40001/doc/go_mem.html
File doc/go_mem.html (right):

https://codereview.appspot.com/101330056/diff/40001/doc/go_mem.html#newcode63
doc/go_mem.html:63: Any such data race results in <i>undefined
behavior</i>.
Perhaps ironically, the Go spec and memory model docs never define the
term "undefined behavior."

https://codereview.appspot.com/101330056/

[go...@golang.org]

R=r...@golang.org (assigned by r...@golang.org)

https://codereview.appspot.com/101330056/

[Russ Cox]

I am inclined to set a moratorium on all changes to this document. Nothing about a typical Go user's experience is improved by continuing to refine the wording here.

Failing that, at the very least any change needs to be motivated not by hypotheticals but by real examples of compiler analysis or rewrites or optimizations that we do today (or want to do very soon) that are ruled out by the current wording.

Russ

[Dmitry Vyukov]

Ian, can you confirm that gccgo implements current guarantees for
racing memory accesses? If the middle end treats Go code as C code,
that I would expect it to not be the case. As far as I know, gcc
sometimes emits 2 32-bit stores instead of a single 64-bit store on
amd64.

Rick, can you comment something on racy pointer memory accesses versus
concurrent garbage collection? Can races on pointers be a problem?

Russ, do you still want to modify this doc to specify how atomic
operations interact with MM? There is an open issue for that.

[Russ Cox]

If I could, I would replace this entire doc with 

    Go Memory Model

    Use locks and channels. Don't be clever.

People can get way too obsessed with language lawyering here.

Russ

[Rob Pike]

I'd be happy to start the document with:

Go Memory Model

Use locks and channels. Don't be clever.

For thoroughness, the rest of this document explains things in more
detail, but if you need to read this document to decide if your
program is correct, you are being clever.

[Dave Cheney]

LGTM.

[Dmitry Vyukov]

It's not as simple. People can do weird things with channels as well.
And then somebody needs to answer the question whether it's correct
code or not. For example consider:

c := make(chan int, 1)
s := ""
go func() {
s = "foo"
c <- 1
}()
go func() {
select {
case c <- 1:
default:
println(s)
}
}()

This program uses only channels for synchronization. Is it guaranteed
to print "foo"?

[Brad Fitzpatrick]

On Mon, Jun 23, 2014 at 5:06 PM, Rob Pike <r...@golang.org> wrote:

I'd be happy to start the document with:

Go Memory Model

Use locks and channels. Don't be clever.

For thoroughness, the rest of this document explains things in more
detail, but if you need to read this document to decide if your
program is correct, you are being clever.

Yes please!
 

[Brendan Tracey]

On Jun 23, 2014, at 7:06 PM, Rob Pike <r...@golang.org> wrote:

> I'd be happy to start the document with:
>
> Go Memory Model
>
> Use locks and channels. Don't be clever.
>
> For thoroughness, the rest of this document explains things in more
> detail, but if you need to read this document to decide if your
> program is correct, you are being clever.

I know this statement was a joke based on truth, but I am someone who did not have any formal training in concurrent programming, and I work with people who think in parallelism rather than concurrency. I appreciated the detail and technicality in the memory model. It shows a formal way to think about concurrent programming (your talks give the high-level vision).

I don’t know enough about compilers and runtimes to have an opinion about the proposed changes, but I just wanted to say that I appreciate the technicalness of the memory model. I appreciate the desire for it to be legible for most users, but at the same time I appreciate it being correct. Just my two cents.

>
>
> On Mon, Jun 23, 2014 at 5:04 PM, Russ Cox <r...@golang.org> wrote:
>> If I could, I would replace this entire doc with
>>
>> Go Memory Model
>>
>> Use locks and channels. Don't be clever.
>>
>> People can get way too obsessed with language lawyering here.
>>
>> Russ
>

> --
> You received this message because you are subscribed to a topic in the Google Groups "golang-codereviews" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/golang-codereviews/IUWZ5ADlIoY/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to golang-coderevi...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Russ Cox]

On Mon, Jun 23, 2014 at 8:16 PM, Dmitry Vyukov <dvy...@google.com> wrote:

It's not as simple. People can do weird things with channels as well.
And then somebody needs to answer the question whether it's correct
code or not. For example consider:

c := make(chan int, 1)
s := ""
go func() {
  s = "foo"
  c <- 1
}()
go func() {
  select {
  case c <- 1:
  default:
    println(s)
  }
}()

This program uses only channels for synchronization. Is it guaranteed
to print "foo"?

Exactly my point.

Use locks and channels. Don't be clever.

Russ

[Ian Lance Taylor]

On Mon, Jun 23, 2014 at 5:01 PM, Dmitry Vyukov <dvy...@google.com> wrote:
> Ian, can you confirm that gccgo implements current guarantees for
> racing memory accesses? If the middle end treats Go code as C code,
> that I would expect it to not be the case. As far as I know, gcc
> sometimes emits 2 32-bit stores instead of a single 64-bit store on
> amd64.

I don't think the current memory model is intended to guarantee that
given a concurrent read and write that the read will observe either a
non-write or a complete write.

What if you retry this CL without mentioning "code generation
optimizations" in the description? Because I think this CL is mostly
a simplification. It's not obvious that we care about code generation
optimizations in this area. But I think it's fine to simplify this
doc.

Ian

[Russ Cox]

Until there is an actual demonstrated need to change this doc, please don't. Each of us has more useful things to do.

Russ