Concurrency02 Operational
2022-09-25 01:06:04

Intro

Memory Model 可以通过一种 Operational 的方式来定义,在这种定义下,我们可以看到一个结果是如何一步一步产生的。

简单地说,一个并发的系统可以看成是 CPU + 内存 两个模块化的部分共同组成的,其中 CPU 有并发的执行流和线程局部的寄存器,内存则可以和 CPU 交互进行读写。这么做的好处在于:

  1. CPU 通常没有太大的变化,可以单独抽象出来定义好,后续直接复用
  2. 内存通过接口与 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 还是很简单的,重点在于 CASFAA

CAS(x, e1, e2)

即 Compare-And-Swap。含义为

  1. 返回内存中的值与 e1 比较的结果
  2. 如果相等,就写入 e2

需要注意的地方有两点:

  1. 此处的接口用的形式为 U(x, v1, v2),含义为“x读到v1,写入v2
  2. 如果不符合条件只会产生 R(x, v1) 的接口
  3. CAS 通常会作为一个同步操作,这点在后面可以看到

FAA(x, e)

即 Fetch-And-Add

Fence

一类特殊的指令,可以看成是对内存的状态控制指令。

Whole

系统作为整体的 step 可以分为

  1. CPU 内部进行计算
  2. 内存内部进行状态的维护
  3. CPU 与内存通过接口进行交互,共同走一步

通常把1、2叫做 silent transition,因为对外界而言它们是不可感知的。

然后就没了,那个习题挺简单的。