Inquiry on Go memory model

[Shi Zheng]

Dear Go developers,

I hope this message finds you well. We are a research team from National University of Singapore and Aarhus University, and we are currently exploring the Go concurrency memory model and its definition of data races. We have come across some behaviors that strike us as odd, so we would appreciate your help in understanding them.

The Go memory model defines an execution of a Go program to be racy if it contains two conflicting events that are unordered by the Happens-Before (HB) relation. This is inspired from the memory models of other programming languages that use shared memory for communication (for e.g., C/C++). The definition of HB, though is defined slightly differently to account for synchronization over channel communication.

We observed that, the definition of HB in the context of Go seems to allow for some paradoxical situations. In the following, we list two such examples:

1. There is a program which will be deemed racy as per the current memory model of Go, but intuitively does not have a data race over any shared memory variable. We illustrate the concrete example program in the attached pdf file (see Fig 1). This program contains a data race as per the Go memory model. However, any execution of this program will ensure that (the only two) conflicting accesses to the (only) shared memory variable x will necessarily be separated in time by other instructions (aka events), due to control-dependence.

2. Another peculiarity is that, unlike the memory models of languages such as C/C++, the Go memory model does not exhibit "compositionality" under data-race freedom. In particular, there are two programs, A and B, that do not share any memory location variables, but do access a common channel (see Fig.2 and Fig.3 in the attached pdf). Individually, neither of these programs is racy (as per the memory model of Go). However, the program obtained by their parallel composition will be deemed to have a data race by the Go memory model (despite the fact that neither A nor B exhibits additional behaviour). Again, we think this is odd, since A and B do not share memory. 

We would like to understand if behaviors like 1. and 2. above are intentional? If so, why? We would greatly appreciate any thoughts and guidance here.

Thank you for your time and assistance!

Best regards,

Zheng Shi

[Jorropo]

That is an interesting edge case, the memory model considers channel receives to be read like. But as you demonstrate a buffered receive is in fact both read-like and write-like.

Do you want to open an issue on https://github.com/golang/go/issues or I can post your findings there ?

--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/golang-dev/SG2PR06MB4868E572C5DE1CBD89726C689F4D2%40SG2PR06MB4868.apcprd06.prod.outlook.com.

[Ian Lance Taylor]

It was not a goal for the Go memory model to say that some programs
are racy even though they are not. However, it was a goal of the
memory model to be easy for programmers to understand how to write
correct programs.

I agree that in your implicit_sync.go program there can't be an actual
memory race. As far as I can tell, the program must always print
nothing or print 1. I also agree that the Go memory model says that
there is a race in the program.

I don't think that we should find this troubling. As the memory model
says: "If you must read the rest of this document to understand the
behavior of your program, you are being too clever. Don't be clever."
That is a guideline, not a joke. If someone sent me a program like
your implicit_sync.go, I would tell them to rewrite it. Nobody should
write code that way, whether the memory model permits it or not.

So from my perspective the questions you raise are interesting only in
the purely academic sense. It's fine to talk about them, and it's
possible that the discussion will lead to some subtle refinement of
the memory model document. But they should have no effect on the
choices made by actual programmers writing actual programs. And if a
modification to the Go memory model causes people to start writing
programs like this, I would consider that to be a failure, and would
argue against making such a change.

To be clear, these are just my personal views.

Ian

[Dan Kortschak]

On Fri, 2024-10-25 at 12:50 -0700, Ian Lance Taylor wrote:
>
> I don't think that we should find this troubling.  As the memory
> model
> says: "If you must read the rest of this document to understand the
> behavior of your program, you are being too clever.  Don't be
> clever."
>  That is a guideline, not a joke.  If someone sent me a program like
> your implicit_sync.go, I would tell them to rewrite it.  Nobody
> should
> write code that way, whether the memory model permits it or not.

To extend this, when thinking about these kinds of things in practice,
I find it helpful to break races into two categories, data races and
logic races. Data races are nice, because the runtime can do a pretty
good job of helping you find them with the race detector. Logic races
are nasty because they do not contain a detectable data race condition.
In the case of the programs here, even if they were not data races,
they are logic races and so should be avoided.

Dan

[Alan Donovan]

In what sense is the program in Figure 3 a parallel composition of the two separate programs? To me, a parallel composition of the two main functions would be something like 

 

   ch2 := make(chan struct{}, 2)

   go func() { a.main(); ch2 <- struct{} }

   go func() { b.main(); ch2 <- struct{} }

   <-ch2;  <-ch2

 

which is race free, both de facto and de jure. The program in Figure 3 causes the two programs to contend for the same channel, which is a much more invasive notion of compositionality, one that I would never expect to work in general.

[robert engels]

I fairly certain it is valid to have multiple readers and writers on a single channel.

--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CACKEwjF6hZMzxxMpHd1BRGUqQEUmqf_DGwTffiPp6XmCTSBypQ%40mail.gmail.com.

[Alan Donovan]

On Fri, 25 Oct 2024 at 17:47, robert engels <ren...@ix.netcom.com> wrote:

I fairly certain it is valid to have multiple readers and writers on a single channel.

A channel may have multiple readers and writers, certainly, but that does not mean that you can arbitrarily fuse two programs that each use a channel so that they now share a single channel.

[Shi Zheng]

Thanks everyone for the responses so far.

1. @Ian, the program implicit_sync.go is just a code snippet aiming at illustrating how the memory model can reject a valid-looking program. It is not clear to us what constitutes bad practice in it, or how one can argue that this communication pattern should not arise in any context.
   
   Of course, as @Dan points out, this program has a “logical race” in the sense that there is a race condition in it (that is, the order of execution affects global program behaviour), but race conditions are natural and abundant in concurrent programming.
   
   

2.  @Alan, by parallel composition we mean that the two programs execute on the same resources (channel/shared memory). One would still expect certain compositionality properties to hold in this setting under specific conditions. To phrase it differently (see the new version of the pdf document attached):
   
   In Fig 2, we now have an execution \sigma_1  in Fig.2 (a) that is race-free according to the memory model. Now we modify execution \sigma_1 to obtain the execution \sigma_2 in Fig.2 (b) by including a new thread (t3) executing a channel-send event. We would expect that this modification (composition of two executions, the initial one and the one from t3) preserves race-freeness, yet execution \sigma_2 is racy (according to the memory model). Again, we do not expect all compositions to preserve race-freeness, but compositions of this particular scheme should.
   
   

3. @Jorropo, we tried to communicate this message to https://github.com/golang/go/issues/69821 but the issue was closed. To us, these issues are important enough to merit a revision in the memory model, but of course, we do not make the call. If you agree, kindly open the issue, and we will follow along the discussion.

[Ian Lance Taylor]

On Mon, Oct 28, 2024 at 7:41 AM Shi Zheng <zheng...@gmail.com> wrote:
>
> @Ian, the program implicit_sync.go is just a code snippet aiming at illustrating how the memory model can reject a valid-looking program. It is not clear to us what constitutes bad practice in it, or how one can argue that this communication pattern should not arise in any context.

I'm arguing based on programming style. You say that your
implicit_sync.go is "a valid-looking program." Personally I would say
that no, it is not. It is a program that looks invalid, because it
appears to have a read/write race on the variable x. For this program
it turns out that we can use careful reasoning, based on the fact that
the channel is buffered and that there is a conditional test of the
value received from the channel, to show that there is no read/write
race. If I have to think that hard to determine that a program that
appears to be invalid is actually valid, then the program is too
complicated.

There are languages that encourage writing complex programs in order
to get the best possible performance. Go is explicitly not one of
those languages. Go encourages writing simple programs that are easy
to understand and easy to see that they are correct. The performance
of Go programs is important but it is not the highest priority of the
language and ecosystem.

So I don't see a reason to complicate the Go memory model to make it
possible to prove, based on the memory model, that this sort of
program does not have a race condition.

This is a personal and subjective opinion. Other people may have
different intuitions here.

Ian

[Jorropo]

One interesting slightly offtopic thing, if channels were not primitives but either as defined as assembly of mutexes &| atomics this problem goes away.

This does not follow the previous stated goals of helping people to write race free programs. That is at least how I reason since I learnt before the memory model was an available resource.

--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAOyqgcUPuhdT5nbCPM7hFcLwpiy%3DLjkg8Ue4yX5aXjvEsg5LPA%40mail.gmail.com.

[Alan Donovan]

On Mon, 28 Oct 2024 at 10:41, Shi Zheng <zheng...@gmail.com> wrote:

1.  @Alan, by parallel composition we mean that the two programs execute on the same resources (channel/shared memory). One would still expect certain compositionality properties to hold in this setting under specific conditions.

Why would one? The concurrency safety of the program depends on the specific data values sent over the channel, so it is entirely unsurprising to me that another thread sending arbitrary new values on that channel might cause the program to misbehave, even if that thread's use of the channel is not by itself racy.

The channel is part of the representation of a data structure whose invariants must be preserved by all who access it. It is not for nothing that we advise against exposing channels in public APIs except when the API must expose concurrency and synchronization to its clients. (For example, if an API just wants to deliver a sequence of values to the client, it is better for it to accept a func value that it repeatedly calls sequentially--even if both producer and consumer are in fact concurrent programs.)

[robert engels]

I think the issue is that the race detector is reporting it as a race, but the combinatory properties state this should not be the case. You might get a program that doesn’t behave as designed, but it wouldn’t be due to a memory barrier based issue.

--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CACKEwjGzQkvBjsHpbDsot8yfnJZZ4ceDcQ3Zda8o0U1vpQ9EhQ%40mail.gmail.com.

[burak serdar]

I believe the problem with the memory model is around how
happened-before is defined for buffered channels. That is: the memory
model defines the write-like operation for a channel read as the
operation that sends the value that was read. But for a buffered
channel, this is not correct. For a buffered channel, the write-like
operation is actually the completion of a read-like operation that
makes the value the next one to be read. That is:
ch <- 1
ch <- 2 --> GMM says this is the write-like operation
x=1
<-ch --> But this is the real operation that makes the value '2'
available to be received next.

> To view this discussion visit https://groups.google.com/d/msgid/golang-dev/E0BEFFE4-D226-4192-99BA-D6A0A1356142%40ix.netcom.com.

[Ian Lance Taylor]

On Mon, Oct 28, 2024 at 1:14 PM burak serdar <bse...@computer.org> wrote:
>
> I believe the problem with the memory model is around how
> happened-before is defined for buffered channels. That is: the memory
> model defines the write-like operation for a channel read as the
> operation that sends the value that was read. But for a buffered
> channel, this is not correct. For a buffered channel, the write-like
> operation is actually the completion of a read-like operation that
> makes the value the next one to be read. That is:
> ch <- 1
> ch <- 2 --> GMM says this is the write-like operation
> x=1
> <-ch --> But this is the real operation that makes the value '2'
> available to be received next.

The current rules from https://go.dev/ref/mem are "A send on a channel
is synchronized before the completion of the corresponding receive
from that channel" and "The kth receive on a channel with capacity C
is synchronized before the completion of the k+Cth send from that
channel completes". It sounds like you are suggesting that we add
something like "the kth receive on a buffered channel is synchronized
before the (k+1)th receive". Is that the general idea?

Ian

[burak serdar]

That sounds obvious, but I think that's it. I was thinking more like:
all send_k and receive_k operations happen before receive_(k+1)

Also note that, based on the example, a channel read from a buffered
channel is both a read-like and a write-like operation. Receiving from
a buffered channel makes the next item in the channel available (hence
the write). It is at that moment the write operation happens, not when
that value is pushed to the channel.

>
> Ian

[robert engels]

Fwiw, in Java, the BlockingQueue which is similar in usage to Channels, states:

Memory consistency effects: As with other concurrent collections, actions in a thread prior to placing an object into a BlockingQueue happen-before actions subsequent to the access or removal of that element from the BlockingQueue in another thread.

-- 
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAMV2RqqQRYHzY_Q--S3bTajnt4AxMTy6wwsKQx-nQ5-N_%2B%3DDKg%40mail.gmail.com.

[burak serdar]

On Mon, Oct 28, 2024 at 4:09 PM robert engels <ren...@ix.netcom.com> wrote:
>
> Fwiw, in Java, the BlockingQueue which is similar in usage to Channels, states:
>
> Memory consistency effects: As with other concurrent collections, actions in a thread prior to placing an object into a BlockingQueue happen-before actions subsequent to the access or removal of that element from the BlockingQueue in another thread.

That has the same problem with the Go memory model. What I was
suggesting can be translated as "actions that move an object to the
front of a blocking queue happen before the removal of that element
from the blocking queue". The java definition also misses the events
that happen after the object is put onto the queue but before it is
removed.

[Keith Randall]

I'm not sure we want to provide any promises about channel reads synchronizing with each other. I can imagine channel implementations which could satisfy multiple reads simultaneously and would need extra synchronization to make this extra promise.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAMV2Rqp4wsyGcW%2Br59GVdXOYnG%2BfV9Bqu6Dv9yusEXY1E2KqRw%40mail.gmail.com.

[robert engels]

AFAIK, that is by design for both performance reasons and reasonability concerns. What you are suggesting would be very hard (impossible?) to implement.

For example,

T1 places A into Q. (event1)
T1 changes arbitrary variable X1…n to Z1…n
T2 reads A from Q.
T2 read any X1…n

According to what you wrote, there would need to be a memory fence after every operation to write X1…N - this only makes sense if they are atomics, and then it doesn’t matter, as atomics provide happens-before anyway.

How would the compiler even be able to determine when the fences should be issued, as ANY code could be executed after (event1) that would need to be happens-before consistent by any read by T2. I don’t think its possible.

[burak serdar]

The problem is not how to implement this. The problem is that the
programs posted are race-free even though the go memory model thinks
that they are. What I am suggesting is a change to the go memory
model, not a change to the implementation. The memory model is
unnecessarily restrictive than the implementation, it defines a
condition as racy even though it is not.

[Keith Randall]

On Mon, Oct 28, 2024 at 4:21 PM burak serdar <bse...@computer.org> wrote:

The problem is not how to implement this. The problem is that the
programs posted are race-free even though the go memory model thinks
that they are. What I am suggesting is a change to the go memory
model, not a change to the implementation. The memory model is
unnecessarily restrictive than the implementation, it defines a
condition as racy even though it is not.

The memory model is unnecessarily more restrictive than the *current* implementation.

The problem is not how to implement the new semantics, as they are implemented by the current Go. The problem is how the new semantics would constrain future implementations of Go.

(That's *a* problem. I think Ian's reservations are more the main point.)

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAMV2RqryaO9mzyCvhmk%2BcLEhs8BH5d8%3DyFVMpHtd3dpoaT3WYQ%40mail.gmail.com.

[robert engels]

Yes, but changing it to what you suggest

>>> "actions that move an object to the
>>> front of a blocking queue happen before the removal of that element
>>> from the blocking queue". The java definition also misses the events
>>> that happen after the object is put onto the queue but before it is
>>> removed.

The queue/channel memory barrier occurs on the initial put and the get - it can’t possibly include any writes that occur after the initial put into the queue - mainly because “any events that happen after the object is put” is asynchronous to the eventual read, so for example:

1. T1 puts A in Q
2. T1 changes X to 100
3. T2 reads A from Q
4. T2 reads X

At step 3 there is no guarantee that step 2 has occurred - which would mean that X could contain any value - steps 2 and 4 are independent events at this point - there is no fence/synchronization point.

So even if the memory model were changed, you still couldn’t reason about the value of X in step 5 - which would mean this would be inherently racy anyway.

Meaning changing the memory model in this way doesn’t solve anything. Even if you could make the read in 3 perform some sort of global synchronization point, and full memory flush across all cores, you couldn’t reason about the value of X - and the performance would be horrendous.

[Keith Randall]

On Mon, Oct 28, 2024 at 4:34 PM robert engels <ren...@ix.netcom.com> wrote:

Yes, but changing it to what you suggest

>>> "actions that move an object to the
>>> front of a blocking queue happen before the removal of that element
>>> from the blocking queue". The java definition also misses the events
>>> that happen after the object is put onto the queue but before it is
>>> removed.

The queue/channel memory barrier occurs on the initial put and the get - it can’t possibly include any writes that occur after the initial put into the queue - mainly because “any events that happen after the object is put” is asynchronous to the eventual read, so for example:

1. T1 puts A in Q
2. T1 changes X to 100
3. T2 reads A from Q
4. T2 reads X

At step 3 there is no guarantee that step 2 has occurred - which would mean that X could contain any value - steps 2 and 4 are independent events at this point - there is no fence/synchronization point.

So even if the memory model were changed, you still couldn’t reason about the value of X in step 5 - which would mean this would be inherently racy anyway.

Meaning changing the memory model in this way doesn’t solve anything. Even if you could make the read in 3 perform some sort of global synchronization point, and full memory flush across all cores, you couldn’t reason about the value of X - and the performance would be horrendous.

I don't think anyone is arguing that this program should work. It is racy in both the old and new semantics.

The new semantics are some sort of sync between different reads of the channel. There's only one read of the channel in your program.

Unless I'm misunderstanding something.

I agree if your program is guaranteed to read 100 in step 4, that would be expensive to implement.

 

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/F7DBF4CA-DDDB-4351-9EBD-59B3A6E3AA56%40ix.netcom.com.

[burak serdar]

On Mon, Oct 28, 2024 at 5:34 PM robert engels <ren...@ix.netcom.com> wrote:
>
> Yes, but changing it to what you suggest
>
> >>> "actions that move an object to the
> >>> front of a blocking queue happen before the removal of that element
> >>> from the blocking queue". The java definition also misses the events
> >>> that happen after the object is put onto the queue but before it is
> >>> removed.
>
> The queue/channel memory barrier occurs on the initial put and the get - it can’t possibly include any writes that occur after the initial put into the queue - mainly because “any events that happen after the object is put” is asynchronous to the eventual read, so for example:
>
> 1. T1 puts A in Q
> 2. T1 changes X to 100
> 3. T2 reads A from Q
> 4. T2 reads X
>
> At step 3 there is no guarantee that step 2 has occurred - which would mean that X could contain any value - steps 2 and 4 are independent events at this point - there is no fence/synchronization point.

The fix I am talking about would be more like:

1. T1 puts A in Q

2. T1 puts B in Q
3. T1 changes X to 100
4. T2 reads A from Q
5. T2 reads B from Q

At step 5, it is guaranteed that step 3 occurred. But this is a race
according to the current memory model, because the write event for
step 5 is at step 2. But the implementation is such that the write
event for step 5 is the read evet at step 4.

[Keith Randall]

On Mon, Oct 28, 2024 at 6:26 PM burak serdar <bse...@computer.org> wrote:

On Mon, Oct 28, 2024 at 5:34 PM robert engels <ren...@ix.netcom.com> wrote:
>
> Yes, but changing it to what you suggest
>
> >>> "actions that move an object to the
> >>> front of a blocking queue happen before the removal of that element
> >>> from the blocking queue". The java definition also misses the events
> >>> that happen after the object is put onto the queue but before it is
> >>> removed.
>
> The queue/channel memory barrier occurs on the initial put and the get - it can’t possibly include any writes that occur after the initial put into the queue - mainly because “any events that happen after the object is put” is asynchronous to the eventual read, so for example:
>
> 1. T1 puts A in Q
> 2. T1 changes X to 100
> 3. T2 reads A from Q
> 4. T2 reads X
>
> At step 3 there is no guarantee that step 2 has occurred - which would mean that X could contain any value - steps 2 and 4 are independent events at this point - there is no fence/synchronization point.

The fix I am talking about would be more like:

1. T1 puts A in Q
2. T1 puts B in Q
3. T1 changes X to 100
4. T2 reads A from Q
5. T2 reads B from Q

At step 5, it is guaranteed that step 3 occurred. But this is a race
according to the current memory model, because the write event for
step 5 is at step 2. But the implementation is such that the write
event for step 5 is the read evet at step 4.

I don't understand how that would work. What's at step 6? Where is the read of X? Is that read guaranteed to return 100?

I don't understand how step 5 guarantees that step 3 occurred. Step 5 only guarantees that step 2 (and step 4) occurred. There is no ordering between step 3 and step (4 or 5).

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAMV2Rqq1XS7ek1Btp1M8PEP6cGAL%3DVdHrDfArKUwOb04C4bcOg%40mail.gmail.com.

[burak serdar]

On Mon, Oct 28, 2024 at 7:36 PM Keith Randall <keith....@gmail.com> wrote:
>
>
> I don't understand how that would work. What's at step 6? Where is the read of X? Is that read guaranteed to return 100?
> I don't understand how step 5 guarantees that step 3 occurred. Step 5 only guarantees that step 2 (and step 4) occurred. There is no ordering between step 3 and step (4 or 5).

I messed up trying to recreate the original problem. Here's the correct version:

1. T1 puts A in Q
2. T1 puts B in Q
3. T1 changes X to 100

4. T1 reads A from Q

5. T2 reads B from Q

6. T2 reads X

According to the Go memory model, 3 and 6 are concurrent, because the
write operation corresponding to the read at step 5 is step 2.
However, the implementation is such that the write operation
corresponding to step 5 is step 4.

[Robert Engels]

The issue is that the ordering of 4 and 5 are indeterminate so without outside locks it is impossible to guarantee the desired constraints.

> On Oct 28, 2024, at 8:43 PM, burak serdar <bse...@computer.org> wrote:

> To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CAMV2RqqNQjXYBkmRG%2BHWpid%2BOitvYDp%2Bv%2B1hXyL-ymz1ue5_3A%40mail.gmail.com.

[Robert Engels]

To clarify, T2 could just as easily read A - then what does that mean?

> On Oct 28, 2024, at 8:52 PM, Robert Engels <ren...@ix.netcom.com> wrote:
>
> The issue is that the ordering of 4 and 5 are indeterminate so without outside locks it is impossible to guarantee the desired constraints.

[burak serdar]

Reminding the original problem:

func main() {
var x int
ch := make(chan int, 2)

go func(ch chan int) {
if <-ch == 2 {
println(x)
}
}(ch)

ch <- 1
ch <- 2

x = 1
<-ch
close(ch)
}

So if the goroutine reads a 2 from the channel, the Go memory model
says it is a data race because read of x and write of x are
concurrent. But they are not. The read from channel after writing x
guarantees that if the goroutine reads 2 from the channel, the read of
x happens after the write of x.

[Robert Engels]

I think that irrespective of the memory model the code may print a value or print nothing at all means it is indeterminate. Seems easier to say the Go race detector does not work for indeterminate programs.

> On Oct 28, 2024, at 9:04 PM, burak serdar <bse...@computer.org> wrote:
>
> Reminding the original problem:

[Keith Randall]

> I think that irrespective of the memory model the code may print a value or print nothing at all means it is indeterminate. Seems easier to say the Go race detector does not work for indeterminate programs.

I don't think indeterminate is the right condition. Perfectly race-free programs can be indeterminate.

    c := make(chan int)

    go func() { c <- 1 }()

    go func() { c <- 2 }()

    println(<- c)

    println(<- c)

can print 1, 2 or 2, 1.

> So if the goroutine reads a 2 from the channel, the Go memory model

says it is a data race because read of x and write of x are
concurrent. But they are not. The read from channel after writing x
guarantees that if the goroutine reads 2 from the channel, the read of
x happens after the write of x.

I think this is a somewhat imprecise re-use of "happens before".

In the Go memory model, "happens before" is a very specific thing. It implies that if A happens before B, then any read after B must see the writes before A.

When you say here "the read of x happens after the write of x", that's true in the "as the clock runs" sense of happens before, but not in the Go memory spec sense. Let's call that "clock before".

This matters, because happens-before in the spec implies a very specific set of memory consistency guarantees. It is not simply the assertion that "if A is clock-before B, then A happens-before B".

A classic example:

var x int

var p *int

go func() { x = 7; p = &x }()

go func() { q := p; if q != nil { println(*q) }}()

If the second goroutine prints something, is it guaranteed to print 7?

Since the second goroutine prints something, then q must not be nil. Which means when it read p, p was not nil. Which means the first goroutine must have gotten past its p assignment. Which means it must have already assigned 7 to x.

So by that argument, the second goroutine must print 7 if it prints. But this is a classic data race. On modern processors this can definitely print values other than 7. The problem here is that although the assignment to p is clock-before the read of p, it is *not* happens-before.

In your example, you've constructed a situation that the read of x is clock-before the write of x, indirectly via a channel operation. Then you're asking why that shouldn't be happens-before also. From my perspective implementing these things, that would imply more guaranteed memory barriers in channel operations than we currently require. Currently the Go channel implementation does all those additional memory barriers almost by accident, by acquiring & releasing a lock on every channel operation. But it doesn't have to. For instance, on processors with write buffers, the current semantics I think don't require a write buffer flush on a channel read. But with the proposed semantics they would. 

Again, this is somewhat academic. I would definitely reject (as in, during code review) any program written to depend on any of the semantics being discussed here. It is just way more confusing than it possibly helps.

We don't want to encourage such programs in any way.

To view this discussion visit https://groups.google.com/d/msgid/golang-dev/7226BE71-AD3D-4C34-B148-654D8579CDC8%40ix.netcom.com.

[Robert Engels]

You’re 100% correct on the indeterminate aspect. 

As to the other, the code I was attempting to provide was in response to the comment that all operations after the put should be visible after a get it if the put value. 

I think this is impossible. The code was designed to show it will always be a data race. 

if that’s not what we were discussing I’m a bit lost :(

On Oct 29, 2024, at 1:04 AM, Keith Randall <keith....@gmail.com> wrote:



To view this discussion visit https://groups.google.com/d/msgid/golang-dev/CA%2BZMcOOWm3cciq5R6R1b53iNP6BUjwF%3DL88ELdCAZLeSWicxMw%40mail.gmail.com.

[Russ Cox]

A lot of this comes down to your practical philosophy and approach to memory models. If you insist on classifying every single program as either racy or race-free, then you can end up lost in the fractal complexity of the boundary between these options. For Go, we admit that there is a muddy middle ground between racy and race-free, containing programs that technically don't have races but also don't fit the definition of race-free. Instead of trying to clean things perfectly and leave behind an intricate boundary that no one will understand anyway, we admit and accept the existence of the mud and advise not wallowing in it.

(This is arguably an instance of the arbiter problem; see Lamport's paper Buridan's Principle for more practical philosophy.)

Best,

Russ

[Shi Zheng]

Thank you everyone for sharing your insights. In our view, issues like the above are important enough to merit a revision of the memory model. It is not clear that a fix would necessarily complicate the memory model (which is a reasonable concern). E.g., some people already appear to think of synchronizing every access on the same channel. This indeed solves the unsound problem in the example program we found. But coming up with the best definition will likely require further thought. 

[Ian Lance Taylor]

On Wednesday, November 20, 2024 at 9:08:55 AM UTC-8 Shi Zheng wrote:

Thank you everyone for sharing your insights. In our view, issues like the above are important enough to merit a revision of the memory model.

 Honest question: why do you think so?  How will this make Go better in

a way that matters for people who use Go?

Ian