又双叒叕拖了一个多月，才把在Madison过圣诞期间在林老师家里的The Go Programming Language读书笔记整理完毕..


从获知各种hardware/language memory model的存在开始，我就一直好奇在业界的各种常用语言中memory model是怎样被定义的。随着了解的深入，我知道了C/C++, Java. 现在轮到了Go.

关于”memory model”的这个概念，我最开始见到的定义大意是「定义在concurrent环境下，一个Read能够读到什么值」。现在我的理解更加注重其目的，它规范了怎样的optimization是valid的。因为人类总想让程序运行得更快，于是提出了一种又一种优化，而优化本身可能在某些条件下能够保持原有语义(semantics)，而在某些条件下却将出现不期望的后果。一个定义好的memory model能够用于规范这些优化，如果some optimization使得原有的正常program出现了memory model不允许的behavior, 就知道它绝对是有问题的了。

科普就到这里，肯定还说的不够清楚.. 不过就先这样吧。接下来，专门记录下书中读到的Go中和此相关的内容，不过并没有完全用代码验证，那些有机会再说吧。

Happen Before

我对Go了解不多，channels似乎是Go中用的挺普遍的一个东西。具体到unbuffered channel, 就是sender在receiver还没有来接收的时候就会blocking wait下去，同理receiver在sender还没有来发的时候也会blocking wait下去。

我说这些的意义是什么呢？这个unbuffered channel可以用来synchronize两个goroutine!!

When a value is sent on an unbuffered channel, the receipt of the value happens before the reawakening of the sending goroutine.

我其实感觉书上说的这个有点奇怪，为啥强调「receiver收到」和「sender恢复运行」这俩时间点呢，而不是去说「sender发出」和「receiver收到」这俩时间点呢？不管了。

而定义的happen before relation其实是很重要的，在各种memory model中，都是定义，如果x happens before y, 则在x时候能够visible的effects, 在y的时候也肯定都能visible. 这里注意，并不是说在x的时候var := 1 is visible, 则在y时候一定是var == 1. 或许其间有一个var := 2的东西发生了，然后在y时刻var := 1和var := 2都是visible, 然后由于其它某些axiom, 选择了var == 2. 我见到的很多axiomatic memory model都是这么定义的。呃.. 我可能越说越乱了..

这本书里关于这些是这样描述的：

when we say x happens before y, … we mean that it is guaranteed to do so and that all its prior effects, such as updates to variables, are complete and that you may rely on them.

有了hb关系之后，也可以据此定义concurrent了，两边互相都不happen-before的话，它俩就是concurrent的。他们可能x先，也可能y先，没有保证的。

Lock/Mutex

在使用lock的时候，unlock()这个操作，和之后获取这个lock的那些个goroutine之间，也是有一个happen-before的关系的。我想起这个是因为Gustavo曾经让我在Coq中写TSO下的semantics, 当时toy language里执行lock/unlock就是需要已经flush完毕buffer的，现在我充分理解了，意义就在于此！

看到这里的时候，书上还描述了reentrant-lock的定义，这是我之前有点弄乱了的？

possible to lock a mutex that’s already locked

Store Buffering?

1
2
3
4
5
6
7
8
9
10
var x, y int
go func() {
	x = 1                   // A1
	fmt.Print("y:", y, " ") // A2
}()

go func() {
	y = 1                   // B1
	fmt.Print("x:", x, " ") // B2
}()

上边是Go语言中写的store buffering program, 这是用来描述TSO与Sequential Consistency区别的经典例子。

在这个例子里，一种可能出现的结果是打印出来的x == 0 ∧ y == 0. 在TSO下，可能的成因是「一开始x := 1以及y := 1的Write都还存在local buffer里没有让所有人都看见」；compiler optimization也可能出现这个问题，可能的成因是简单的reordering, 因为在单独的一个thread看来，Write to x与print y是没有关系，那么为了效率执行顺序是可以调换的。

书中写起这个也是为了介绍这个non-sequential behavior, 这是在向读者举例说明，concurrent条件下，程序猿很容易直观地想象成不同instruction atomically interleaving的情况。然而现实并不是这样运作的..

Coherence?

In the absence of explicit synchronization using a channel or mutex, there is no guarantee that events are seen in the same order by all goroutines.

这个描述里，只是说了“write to different variable”在不同的thread间可以有不同的order, 那么write to same variable呢？是会同样的order的吗？？coherent? 这其实是另一个经典litmus – IRIW (Independent Read, Independent Write)所描述的内容，在书里这儿并没有说。

1
2
3
4
5
6
7
8
9
10
11
12
13
T1:
	x := 1

T2:
	x := 2

T3:
	a := x
	b := x

T4:
	c := x
	d := x

IRIW例子想要看到的最终情况就是，是否可能a == 1 ∧ b == 2 ∧ c == 2 ∧ d == 1. 即在T3和T4的眼中，x的更新顺序是不一样的。例子很极端，普通代码中基本用不到，但是对于完整了解整个memory model的定义/实现是很有意义的。

How Go Reacts

书中介绍了这个几个例子，之后只是引出，在Go中，如果我们stick some programming patterns, 就不需要担心这些个幺蛾子。

Whenever possible, confine variables to a single goroutine; for all other variables, use mutual exclusion.

但是这么说有点废话呀 = =

Go自己也提供了一个race detector. 那么看来，他们显然也提供了DRF guarantee, 即对于data-race-free的program, 可以忽略上边一大串幺蛾子，想象成atomic interleaving (sequential consistency) 就足够了，足以考虑到所有的情况了。

而他们的race detector也只是dynamic的，所以其实并不完备呀：

However, it can only detect race conditions that occur during a run; it cannot prove that none will ever occur.

以我推断，Go至少提供了DRF model, 其它并没有特别明显的东西，也好像没有official formal formalization. 所以就先这样吧。其实官方是有文档的，我只是要强行把笔记整理出来而已 +。+

我只看了这本书中我想要看的ξ8. Goroutines and Channels, 以及ξ9. Concurrency with Shared Variables这两个章节，因为只有这俩是我关心的.. 我现在感觉，Go routine其实和thread没多大差。而Go整个给我的感觉，就像是很多Unix commands用的很开心的程序猿把这些全部融合到一个语言里打包给你，加上其它实际很可能用到的支持。认识还很粗浅，很可能不对，就先这样吧..