Contents
  1. 1. Happen Before
  2. 2. Lock/Mutex
  3. 3. Store Buffering?
  4. 4. Coherence?
  5. 5. How Go Reacts

又双叒叕拖了一个多月,才把在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 := 1var := 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用的很开心的程序猿把这些全部融合到一个语言里打包给你,加上其它实际很可能用到的支持。认识还很粗浅,很可能不对,就先这样吧..

Contents
  1. 1. Happen Before
  2. 2. Lock/Mutex
  3. 3. Store Buffering?
  4. 4. Coherence?
  5. 5. How Go Reacts
comments powered by Disqus