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，因为对外界而言它们是不可感知的。
然后就没了，那个习题挺简单的。