KAIST-CS431: Promising Semantics

本章是基于作者的研究“Promising semantics”: https://sf.snu.ac.kr/promise-concurrency/ ，提出的一种对宽松内存（relaxed-memory）并发的建模方法。

主要观点有4个：

modeling load hoisting w/ multi-valued memory
- 允许一个线程从某个位置读取到一个旧值
modeling read-modify-write w/ message adjacency
- 禁止对单个值同时进行多个read-modify-write操作
modeling coherence & ordering w/ views
- 限制线程的行为
modeling store hoisting w/ promises
- Allowing a thread to speculatively write a value

个人理解，**即便是编译器/硬件的指令重排，也是需要遵循一定的规则的，不能随意乱排。**作者从值读取、存储、read-modify-write多种角度对线程的行为进行了建模，是为了解释哪些情况下出现多线程执行出现哪些结果是可能的，哪些是不被允许的。

hoisting load/store在网上没有搜到解释，但是有个gcc的优化提到了这个概念。大概意思时将存值/取值操作从原先的指令顺序中调整位置，优化执行效率。

Load/Store Hoisting - GNU Project

multi-value memory#

内存是一系列消息（message）所在的位置，而消息可以看作是值和时间戳的组合。线程很有可能在读取时从内存中读到一个旧值。（effectively hoisting loads）

在作者举的例子中，r1=r2=0是被允许的，因为r1 r2都有可能从Y X中读到一个旧值。从后文的view角度理解，因为在独立的线程中，X和Y的赋值并没有改变当前线程中相应Y和X的view，所以，r1 r2的读取操作是可以读到旧值的。

message adjacency#

上面说了，消息是值和时间戳范围的组合。read-modify-write操作修改了消息的值，在时间轴上应该和前值紧邻在一起（no gap）。

可以看到，两次fetch_add操作后，从X的视角上看，0、1、2是紧邻的。第二次fetch_add操作，只能紧贴着1操作，而不能插到0和1之间。

views#

这个semantics对我是启发性最强的一章。

multi-valued memory允许了太多不在预期中的行为，因此我们需要做些限制，保证一致性和同步。

View分为三种，分别是：

Per-thread view：一致性
Per-message view：release/acquire同步
Global view：SC同步

Per-thread view#

Per-thread view表示线程对消息的确认。

如上图示例，初始情况下，X=0，Y=0。

```
X = 1 || r1 = X; r2 = X
```
- [RR coherence]：在左边线程赋值后，右边线程进行两次读操作。因为左右线程均是独立视角，所以右边线程读取时，只会有X=0,Y=0或者X=1,Y=0两种view。如果r1=1，那么r2读取时view必定为X=1,Y=0，所以r1=1,r2=0是不可能出现的；
```
r=X; X=1
```
- [RW coherence]：同一个线程中，如果在X赋值之前进行读取，r只能看到X=0的view，所以r=0；即X=1不可能重排到r=X读取指令之前；
```
X=1; r=X
```
- [WR coherence]：同一个线程中，先赋值后读取，那么读取操作只能看到赋值之后的view，也就是r=1；
```
X=1; X=2
```
- [WW coherence]：同一个线程中，后赋值必定覆盖先赋值语句，即执行完成后，X=2。

总结：

读写操作应当发生在当前线程的view之后，也就是说，view之前的值是不能被当下的读写操作获取的；
读写操作改变了当前线程的view。在读写操作后，view就由读写操作确定的新值决定。后续的读写只能在这个新的view之后；

线程视角给予了重排一定的基本约束，即便发生重排，最终执行的效果也是看起来和没有重排一样。

Per-message view#

Per-message view representing the released view of the corresponding store。可以用来对release/acquire模型建模。

X = 1;                ||   if Y.load(acquire) {
Y.store(1, release);  ||       assert(X == 42);
                      ||   }

初始状态下，左边线程和右边线程的视角都为X=0, Y=0。

在执行完X=1后，左边线程的视角切换成X=1, Y=0。

执行完Y.store(1, release)后，左边线程视角切换成X=1, Y=1。对于released message来说，它的视角和当前线程的视角是一样的，X=1, Y=1。

在右边线程执行Y.load(acquire)后，实际上完成了一次message passing。将message的视角同步给右边线程，所以，此时右边线程的视角也是X=1, Y=1。最终assert成功。

总结：release/acquire实际上是强制将release线程的视角同步给了acquire线程，实现访存一致性。release/acquire起到了message passing的作用。

Global view#

A global view representing the currently accumulated view of SC fences。SC是sequentially consistency（序列一致性）的缩写。

X = 1;                ||   if Y.load(relaxed) {
fence(SC);            ||       fence(SC);
Y.store(1, relaxed);  ||       assert(X == 1);  }

同样，初始状态下，左边线程和右边线程的视角都为X=0, Y=0，执行完X=1后，左边线程的视角切换成X=1, Y=0。

在执行完fence(SC)后，SC的视角和当前线程的视角保持同步，X=1, Y=0。

执行完Y.store(1, relaxed)后，左边线程的视角发生变化，X=1, Y=1，SC视角因为没有执行同步，保持不变。

在右边线程执行完Y.load(relaxed)后，线程视角变为X=0, Y=1。

而在右边线程执行完fence(SC)后，SC视角同步当前最新的变化，即X=1, Y=1，同时也将该视角同步给右边线程。最终assert成功。

总结：SC view就像序列一致性一样，每次执行fence(SC)后，将当前线程的变更同步到一个全局统一的视角中，而同时也会将SC视角中的变化同步到当前的线程上，完成message passing。

promises#

promises语义用来对store hoisting建模。promises建模的目标是只允许**==语义上独立的写操作（semantically independent writes）==**进行hoisting。什么叫语义上独立的写操作？作者介绍了三种场景：

Store hoisting without dependency
Store hoisting with dependency
Store hoisting with syntactic dependency

在这些场景中，哪些可以进行store hoisting，哪些不能进行。作者提出的思路是**==语义上独立的写操作始终会在未来的某个时刻写入==**。具体来说，有如下两个步骤：

线程可以预期去写入一个值（“promise to write”）；
线程应该能够始终在未来某个时刻写入它的promises。

概念有点绕，我们可以通过上面的三种场景来理解作者的这种思路。

Store hoisting without dependency#

所谓的Store hoisting without dependency，就是指在线程中没有其他的指令对store操作有影响。

r1 = X    ||    r2 = Y
Y = r1    ||    X = 1

上面的例子可以看到，左边线程Y=r1很明显是对上一条指令r1=X有依赖的。但是右边线程的两条指令就没有关联。从线程的view上看，右边线程可以进行store hoisting，将X=1先执行，所以最终结果r1=r2=1是允许的。

作者在这里采取了另外一种建模方式。首先我们从右边线程的独立视角去执行，最终可以得到X=1, Y=0的视角。于是X会预期写入1（certified），见下图。

在实际执行时，左边线程读到Certified的view，X=1, Y=1。

右边线程执行r2=Y，视角如上图。此时，X=1是在线程视角右侧，是允许写入的。

所以X=1 Re-certified成功，允许r1=r2=1的结果。

Store hoisting with dependency#

r1 = X    ||    r2 = Y
Y = r1    ||    X = r2

按照上一节的建模方法，我们看右边线程视角时无法对X=1进行Certified，也就没有promised，拿不到r1=r2=1（感觉这个例子有点奇怪，因为始终没有对X/Y=1的赋值）。从线程的视角上看，两边线程也都受到RW coherence的约束。

Store hoisting with syntactic dependency#

r1 = X    ||    r2 = Y
Y = r1    ||    if r2 == 1 { X = r2 }
          ||    else       { X = 1 }

这个例子是最能够理解作者的promises思路的。我们按照Store hoisting with dependency中的步骤来看。

在右边线程的独立视角中，r2=Y=0，所以进入else分支，X=1，能够Certified。

同样，左边线程执行完后，右边线程给r2赋值，得到r2=Y=1，X=0的视角。

此时，进入if分支，X=r2=1，能够Re-certified。所以r1=r2=1的结果是被允许的。

==Certification and real execution may diverge to capture semantic dependency only.==

r1 = X    ||    r2 = Y; r3 = X
Y = r1    ||    if r2 == 1 { X = r2 }
          ||    else       { X = 1 }

如果在上面的例子扩展一下，加上r3=X；此时Certified没问题，但是在re-certified时，由于r3的读取操作，使得此时右边线程的视角是X=1, Y=1，而写入操作只能在当前线程视角的右侧，所以X=r2=1无法写入，re-certified失败。r1=r2=r3=1是不被允许的。从另外一个角度来看，r3=X的使得右边线程加入了RW coherence，X=1的指令无法重排到r3=X之前。

总结#

这一章实际上是作者从理论建模的角度分析了什么时候能够进行指令重排，对于分析硬件/编译器行为是很有用的。尤其是通过线程视角和全局视角来分析多线程的读写操作，启发性很大。