memory model bug

[rsc]

from private mail:

'''A read r of a variable v is allowed to observe a write w to v if
both of the following hold:
  1. w happens before r.
   2. There is no other write w' to v that happens after w but before r.

 A read r of a variable v is also allowed to observe a write w to v
if  w happens    concurrently with r.

 If a w does not fit into either of these two cases,  a read r of
variable v is guaranteed to not observe the write w to v.
'''

from golang-nuts (same issue):


---------- Forwarded message ----------
From: Andrew Hart <hartandrewr@gmail.com>
Date: Tue, Sep 20, 2011 at 01:29
Subject: [go-nuts] Go Memory Model: allowed
To: golang-nuts <golang-nuts@googlegroups.com>


go_mem.html states
> A read r of a variable v is allowed to observe a write w to v if both of the
following hold:
> 1. w happens before r.
> 2. There is no other write w' to v that happens after w but before r.

This definition doesn't seem necessary for the rest of the document.
One line seems to contradict it:
> Note that a read r may observe the value written by a write w that happens
concurrently with r. Even if this occurs, it does not imply that reads happening after r
will observe writes that happened before w.

If "w happens concurrently with r" is true, then "w happens before r"
is false by definition.

A more consistent definition of allowed might replace the first
condition with:
1. r does not happen before w

Should such a replacement be considered?

What motivates defining allowed (rather than only defining
guaranteed)?

Leaving "allowed" out of the model entirely might not be bad in light
of some previous posts: http://groups.google.com/group/golang-nuts/msg/ba17c1ab71357629
http://groups.google.com/group/golang-nuts/msg/75caf6fbe3b24cca
http://groups.google.com/group/golang-nuts/msg/8b1adf2a50f0dcb7

Thanks,
Andrew Hart

[rsc]

Comment 1:

This issue was closed by revision 44d13e3.

Status changed to Fixed.

[rsc]

Comment 2:

Issue #3144 has been merged into this issue.