Intro
Memory Model 可以通过一种 Operational 的方式来定义,在这种定义下,我们可以看到一个结果是如何一步一步产生的。
简单地说,一个并发的系统可以看成是 CPU + 内存 两个模块化的部分共同组成的,其中 CPU 有并发的执行流和线程局部的寄存器,内存则可以和 CPU 交互进行读写。这么做的好处在于:
- CPU 通常没有太大的变化,可以单独抽象出来定义好,后续直接复用
- 内存通过接口与 CPU 交互,这样我们就可以简单地替换不同的内存模型观察执行的结果
CPU
这部分没啥好说的,主要是记号的问题。那几个函数的用法倒是挺巧妙的,可以把一些编号的信息 encode 到参数里,这样就看起来很简洁。
Memory
Interface/Label
我到今天都不知道到底是 l 还是 I
注意到这里的 Interface
并不是一种具体的行为,而是描述了一个结果,即这部分与细节无关,仍然是
declarative 的。具体以 U(x, v1, v2)
举例。
U(x, v1, v2)
例如有条规则长这样 \[ \frac{I\text{=U(x,s($e_r$),s($e_w$))}} {\text{r:=}\bold{CAS}\text{(x,$e_r$,$e_w$)},s\overset{I}\Rightarrow \bold{skip},s[r\mapsto1]} \] 可以发现 CPU 在获得内存返回值之前是不可能更改寄存器的值的,同理内存在获得 CPU 提供的值之前也不可能返回比较的结果,因此者无论如何都不是一次通信就可以实现的。
而这个接口记号的真正意义在于,它只描述了最后二者达成的共识:内存读到了 \(s(e_r)\),写入 \(s(e_w)\),具体的实现则无关紧要,并且这个结果的达成本身是原子的。
这部分讲得比较绕,但大概意思是这样。
Rules
线程内部的 step rules 还是很简单的,重点在于 CAS
和
FAA
CAS(x, e1, e2)
即 Compare-And-Swap。含义为
- 返回内存中的值与
e1
比较的结果 - 如果相等,就写入
e2
需要注意的地方有两点:
- 此处的接口用的形式为
U(x, v1, v2)
,含义为“x
读到v1
,写入v2
” - 如果不符合条件只会产生
R(x, v1)
的接口 - CAS 通常会作为一个同步操作,这点在后面可以看到
FAA(x, e)
即 Fetch-And-Add
Fence
一类特殊的指令,可以看成是对内存的状态控制指令。
Whole
系统作为整体的 step 可以分为
- CPU 内部进行计算
- 内存内部进行状态的维护
- CPU 与内存通过接口进行交互,共同走一步
通常把1、2叫做 silent transition,因为对外界而言它们是不可感知的。
然后就没了,那个习题挺简单的。