Go Memory Model question

[のびしー]

Hello, I have another question regarding the Go Memory Model.

(1) Can this program print "10", according to the Memory Model?
(2) If that is forbidden, which part of the Go Memory Model excludes such behavior?

https://go.dev/play/p/Fn5I0fjSiKj

```go
package main

var x int = 0

func main() {
go func() {
x = 1
}()
print(x) // first read: 1
print(x) // second read: 0
}
```

I draw a picture of the happens-before relation of this program here:

https://gist.github.com/nobishino/8150346c30101e2ca409ed83c6c25add?permalink_comment_id=4388680#gistcomment-4388680

I think the answer to (1) is yes.
Both reads are concurrent with x = 1, so each read can observe both x = 0 and x = 1.
And there is no constraint between the results of the first read and the second read.
So the second read can observe x = 0 even if the first read observes x = 0.

But I'm not very sure. Is this understanding correct?

[のびしー]

> So the second read can observe x = 0 even if the first read observes x = 0.

Sorry, I meant "So the second read can observe x = 0 even if the first read observes x = 1." here.

2022年12月2日(金) 21:10 のびしー <nobis...@gmail.com>:

[peterGo]

Programs that modify data being simultaneously accessed by multiple goroutines must serialize such access.  

https://go.dev/ref/mem  

$ go run -race racer.go
00
==================
WARNING: DATA RACE
Write at 0x00000054d5f8 by goroutine 6:
  main.main.func1()
      /home/peter/racer.go:7 +0x29

Previous read at 0x00000054d5f8 by main goroutine:
  main.main()
      /home/peter/racer.go:9 +0x3c

Goroutine 6 (running) created at:
  main.main()
      /home/peter/racer.go:6 +0x30
==================
Found 1 data race(s)
exit status 66
$

peter

[Axel Wagner]

I believe your example is basically equivalent to the ones in https://go.dev/ref/mem#badsync which also contains an explanation of how the memory model implies this (or rather, how it does not imply the opposite).

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAGoET5HyPxEhBETGWNPuYpDgXbm0JM3jeaKFdoQdtc5eGUR0Uw%40mail.gmail.com.

[のびしー]

> I believe your example is basically equivalent to the ones in https://go.dev/ref/mem#badsync which also contains an explanation of how the memory model implies this

@Wagner

Thanks for your opinion, I think so too. I was not confident that my example is equivalent to https://go.dev/ref/mem#badsync, since my example reads from the same variable.

> Programs that modify data being simultaneously accessed by multiple goroutines must serialize such access. 

@peterGo

I know that my example has data races. But the Go Memory Model guarantees a limited number of outcomes for programs with races(unless runtime reports the race and terminates). My question is about the limited outcomes.

2022年12月2日(金) 22:02 Axel Wagner <axel.wa...@googlemail.com>:

[burak serdar]

The way I read the memory model, this program can print 01, 00, and 11, but not 10. This is because goroutine creation creates a synchronized before relationship between x=1 and x=0, so even though there is a race, x=0 happens before x=1.

To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAGoET5Fk6Wwd7JOJOY%3DJVix9NymsP3yJ_P%2BaDPgtPTorL-X_Wg%40mail.gmail.com.

[Quân Anh Mai]

A. From the theoretical point of view given this program:

Initial:

x = 0

Thread 1:

x = 1

Thread 2:

x1 = x

x2 = x

If x1 = 1, we have the following happen-before relationship:

- x = 0 happens before x = 1

- x = 0 happens before x1 = x

- x1 = x happens before x2 = x

Note that there is no x = 1 happening before x1 = x since these are not synchronising operations.

As a result, there is no happen-before relationship between x = 1 and x2 = x, which means these 2 are racy, and the read can observe either value of 0 or 1.

B. From the practical point of view, given the 2 reads:

x1 = x

x2 = x

The compiler, CPU, etc can freely reorder these 2 operations, which leads to the second load executing before the first one. Worse, even if the first load seems to come before the second one from the perspective of a thread, there is no guarantee that another thread may observe the opposite behaviour, that is the second load may result in some value that apparently impossible at that point. This may lead to paradoxes when trying to reason the behaviour of a program using some sequentially consistent order of a permutation of a program order.

The ability to prevent the reordering of 2 loads with respect to every thread is called a load-load fence. Suppose Go will support memory barriers in the future, your program can be rewritten as:

```go
package main

import "memory"

var x int = 0

func main() {
    go func() {
        x = 1
    }()

    print(x) // first read: 1

    memory.LoadLoadFence()

    print(x) // second read: 0
}
```

and we can hope that the program will never print out 1, 0.

Thanks.

[robert engels]

happens-before in this case would only guarantee 0, not 1. e.g. change the initializer to x = 3, then 3 must be guaranteed to be seen rather than the default value of 0

To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAMV2Rqphhx8S0sZDv%3Dj1rskhPvCBstzLo%2BAscz5X7pMnNFzWNQ%40mail.gmail.com.