How can reads on an unbuffered channel be synchronized before writing to the channel?

Golang memory model documentation states the following things:

(1)

Some memory operations are read-like, including read, atomic read, mutex lock, and channel receive. Other memory operations are write-like, including write, atomic write, mutex unlock, channel send, and channel close.

(2)

The synchronized before relation is a partial order on synchronizing memory operations, derived from W. If a synchronizing read-like memory operation r observes a synchronizing write-like memory operation w (that is, if W(r) = w), then w is synchronized before r.

(3)

A receive from an unbuffered channel is synchronized before the completion of the corresponding send on that channel.

The definition of the synchronized before relation (2) states that if the synchronizing read-like memory operation r observes a synchronizing write-like operation w, then w is synchronized before r.

Documentation also states (3) that the receive from an unbuffered channel is synchronized before the send on that channel.

However, what confuses me is if the receiving from a channel is read-like operation (1), how can it be synchronized before its corresponding write. According to definition of the synchronized before relation (2) it could only be the other way around, like in case of buffered channel where send is synchronized before receive.

This contradicts the definition of the synchronized before relation (2).

Am I missing something?

Solution

What you are probably missing is that “A receive from an unbuffered channel is synchronized before the completion of the corresponding send on that channel,”.

Let's examine the example from the memory model (Go Playground):

package main

func main() {
    c := make(chan int)
    var a string

    go func() {
        a = "hello, world"
        <-c // (1)
        // (2)
    }()

    c <- 0 // (3)
    // (4)
    println(a)
}

If a synchronizing read-like memory operation r observes a synchronizing write-like memory operation w (that is, if W(r) = w), then w is synchronized before r.
- (3) is synchronized before (1), we can't read a value before it is written - unimportant in our context
A send on a channel is synchronized before the completion of the corresponding receive from that channel.
- (3) is synchronized before (2), the goroutine can't exit before the value is sent - unimportant in our context
A receive from an unbuffered channel is synchronized before the completion of the corresponding send on that channel.
- (1) is synchronized before (4), a = "hello, world" is sequenced before (1) and println(a) after (4), so println(a) observes the effects of a = "hello, world" without race conditions.

Edit:

Be aware that “x synchronized before y” does not mean that y is execucted immediately after x, only later. You could fit stuff in between.

So, in the example above, assuming you only have one CPU, (3) .. (1) .. (2) .. (4) is valid, or (3) .. (1) .. (4) .. (2), and you can put stuff from any other goroutine that runs concurrently in .., like (3) (x) (1) (y) (2) (z) (4) (t). You only need to keep the order specified.

You can also fit println(a) in, as long as (4) > println(a) due to sequencing. So (3) (1) (4) println(a) (2) is valid, like is (3) (1) (4) (2) println(a).

(1) is sequenced before (2), so (2) ... (1) is not valid.

If we make the channel buffered

package main

func main() {
    c := make(chan int, 1)
    var a string

    go func() {
        a = "hello, world"
        <-c // (1)
        // (2)
    }()

    c <- 0 // (3)
    // (4)
    println(a)
}

We loose “(1) is synchronized before (4)”, since that came from “A receive from an unbuffered channel is synchronized before the completion of the corresponding send on that channel.”

We get instead

The kth receive on a channel with capacity C is synchronized before the completion of the k+Cth send from that channel completes.

Which in our case means nothing at all, since there is no second send.

So, since we are left with only (3) > (1) and (3) > (2) (combined with (1) > (2) and (3) > (4) because of sequencing) (3) .. (1) .. (4) .. (2) is still valid, but (3) .. (4) .. (1) .. (2) now also is. That means we might or might not observe the effect of a = ... at the point of println(a), which is a race condition.

Edit2:

For more on the theoretical foundation you might want to read about Lamport clocks and the blog entries by Russ Cox.