Does "Message Passing" litmus test can fail in Go memory model?

[Nobishii N]

Hello, 

I have read Go1.19(tip) memory model document(https://tip.golang.org/ref/mem)  and have following question. (I think my question is valid for the current model(https://go.dev/ref/mem), though.)

Here is my translation of so-called "Message Passing" litmus test to Go program.

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

Does this program can panic according to the memory model?

I think it can panic according to the model, but I'm not confident because it is subtle problem for me.

My reasoning is as follows.

First of all, this program has data race. Behavior for data races are documented in the section "Implementation Restrictions for Programs Containing Data Races". According to this section, 

- read y := y (L18) can observe both y = 1(L13) and y = 0(initialization at L5)

- read x := x (L19) can observe both x = 1(L12) and x = 0(initialization at L5)

so the result "x == 0 && y == 1" can actually happen, causing this program to panic.

Is my reasoning correct?  

[Ian Lance Taylor]

I agree that this program can panic.

Ian