The Go memory model starts with the following ominous trespassing sign:

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.

Feeling clever? Then come on in! Make sure you have brushed up on the concept of happens-before relation from the previous post.

The Go memory model lays out the rules for what values can be read from memory given previous writes to memory from different threads (or goroutines as they are called in Go). It uses the happens-before relation to precisely describe when a read operation can observe given write. If remember the previous post and are paying super close attention, you will notice that Go defines the happens-before relation slightly different from Lamport. The Go specification says:

  1. Instructions within a thread are in happens-before relation. (Same as Lamport)
  2. A send onto a channel happens-before the corresponding receive from that channel completes. (Almost the same as Lamport)
  3. The $k^{th}$ receive from a channel with capacity $C$ happens-before the $(k+C)^{th}$ send onto that channel completes. (New compared to Lamport)

There are a few other rules not mentioned above, such as rules about spawning new threads (or Go routines). But we don’t need them right now. Rules (0), (1), and (2) above will give us plenty to think about.

Reasoning with the Go memory model

Let us revisit our good old example from our first post on memory models. In case you don’t remember, here you go again:

     T1         |    T2
z    = 42       |   if (done)
done = true     |     print(z)

We saw that this program is properly synchronized given a strong or sequentially consistent memory model. However, under weak memory, T2 can observe T1’s instructions as if they were executed out of program order. Given this swapping of T1’s instructions, the program is not properly synchronized and T2 may print an uninitialized value of z.

Let us reason about the example from the perspective of the Go memory model. Again, we label the statements in the program as A, B, C and D:

     T1            |    T2
z    = 42     (A)  |   if (done)     (C)
done = true   (B)  |     print(z)    (D)

Given rule (0) from the Go memory model, we infer that A $\rightarrow_{hb}$ B and that C $\rightarrow_{hb}$ D. But that is all we get! There is no way to relate events from thread T1 to events of thread T2. Given the fact that the instructions in T1 and T2 are not related by happens-before, it is possible for D to occur before A in an execution.

If we want to fix this program and make sure T2 will necessarily print 42, then we must ensure that A happens-before D. How can we do that?! In Go, we use channels. Let us replace the setting of done and the checking of done with a send on a channel c and a receive from that channel:

     T1            |    T2
z    = 42     (A)  |   <- c        (C)
c   <- true   (B)  |   print(z)    (D)

The statement c <- true, with the arrow pointing into the channel, means that we are sending the value of true on the channel. The statement <- c, with the arrow pointing away from the channel, means we are receiving a value from the channel.

Because the receive operation is blocking, meaning, it will block until there is something to be received, we know that the receive will only occur once the sent has occurred. Indeed, given rule (1) from the Go memory model, which says that “a send happens-before the corresponding receive completes”, we now have B $\rightarrow_{hb}$ C. Thanks to rule (1), we are able to relate events from different threads.

At this point we have:

  • A $\rightarrow_{hb}$ B by rule 1, program-order
  • B $\rightarrow_{hb}$ C by rule 2, send happens-before completion of receive
  • C $\rightarrow_{hb}$ D by rule 1, program order.

By transitivity of the happens-before relation, we can then conclude that A $\rightarrow_{hb}$ D. We have thus reasoned that this program will necessarily print 42. Neat!

Much ado about something

We used the Go memory model and the happens-before relation to analyze a program, we saw that the original program was not properly synchronized. We then used channels to obtain a new program and we employed the happens-before relation to reason about the correctness of this new program.

You may be wondering… that was a lot of work! Indeed. We are building concepts and mathematical tools for reasoning about programming languages and programs. It takes effort. But the effort can have big pay-offs. Later we will see how these same concepts and tools helped expose a bug in Go that was undetected for many years.