Yanyan's Wiki 操作系统 (2022)

共享内存多线程

本讲阅读材料

本讲的阅读材料是本文档 (讲义)。带着 “程序是状态机” 的视角,你不仅可以试着自己画出 Peterson/Dekker/任何算法的状态机,并理解它们能够正确工作的假设和它们正确的原因。“程序 = 计算机系统 = 状态机” 这一理解将贯穿整个《操作系统》课程。

1. 状态机

“状态机” 是对物理世界运行的抽象数学模型。熟悉图论的同学,不妨把状态机看成是有向图 $G(V,E)$,其中:

这个概念非常之简单 (甚至 trivial) 以至于你会觉得它有什么用?答案有两点:

  1. 状态机是物理世界的抽象,几乎任何物理对象都或多或少可以写成状态机。一旦状态机建立,我们就得到了一个图——于是我们可以用图论的算法去研究状态机的性质。例如,当我们写出一个并发程序 (并发算法、并发协议) 的状态机后,就能用图论的语言定义并发程序算法的 “正确性”,并在 $|E|$ 的多项式时间内完成对算法的证明。
  2. 计算机系统的本质天然是数字逻辑电路实现的状态机,因此状态机模型也可以帮助我们理解计算机系统的方方面面。状态机的视角帮助我们理解处理器设计、程序调试、自动测试等 non-trivial 的计算机系统解决方案。

2. 程序的状态机模型

我们不妨把运行在操作系统上的程序看成是状态机。在现代计算机系统上,程序只需要有代码、数据 (假设只有静态分配的数据;动态分配数据需要调用操作系统)、堆栈和寄存器,程序就按固定的规则执行:

在《计算机系统基础》的编程实验中,我们已经切实地体会过这个过程。而在 gdb 中,我们也可以查看 (被暂停的) 进程运行时的状态:

(gdb) info registers   // 查看寄存器
rax            0x55555555463a   93824992233018
rbx            0x0  0
...
rip            0x55555555463e   0x55555555463e <main+4>
eflags         0x246    [ PF ZF IF ]
...
(gdb) x/16i 0x55555555463e   // 查看内存
=> 0x55555555463e <main+4> :  lea    0x9f(%rip),%rdi        # 0x5555555546e4
   0x555555554645 <main+11>:  callq  0x555555554510 <puts@plt>
   0x55555555464a <main+16>:  mov    $0x0,%eax
   0x55555555464f <main+21>:  pop    %rbp
   0x555555554650 <main+22>:  retq   
   ...

如果使用单步执行一条指令,我们将会看到状态的变化,而且状态的变化符合是 rip 寄存器位置指令的行为。因此,我们不妨把所有的寄存器/内存的数值作为程序的状态,程序在两个时刻寄存器/内存数值只要有任何不同,就认为是两个不同的状态。

程序每执行一条指令,状态就会发生变化 (指令执行的结果)。我们用 $(M,R)$ 来表示程序的状态,其中 $M$ 是程序所有内存的数值;$R$ 是程序所有寄存器的数值。例如,假设 $M[R[\textrm{rip}]]$ 的字节序列是 48 c7 c0 01 00 00 00,即 movl $1, %rax。那么,执行这条指令后程序的状态是 $(M',R')$,则有:

$R'[\textrm{rip}] = R[\textrm{rip}] + 7$ (下一条指令位于 7 个字节之后), $R'[\textrm{rax}] = 1$ (rax 寄存器被设置为 1)

考虑程序一共使用 16 MiB 的内存,有 18 个 64-bit 寄存器,这些状态一共有 $16 \cdot 2^{20} \cdot 8 + 18 \cdot 64 = 134,218,880$ bits。因此,这个程序至多有 $2^{134,218,880}$ 种不同的状态。这是个天文数字——试图把程序所有状态构成的状态机建立出来是完全不切实际的。但这不妨碍我们用状态机模型理解程序的执行。

2.1. 确定 (deterministic) 和不确定 (non-deterministic) 的指令

大部分指令在给定执行前的状态时,执行的结果就是确定的,例如 push, mov 都是这样确定的指令。如果 $(M,R)$ 状态下 PC 指针位置的指令是确定的指令,那么 $(M,R)$ 就拥有唯一的后续状态——事实上,程序执行中绝大部分指令都是确定的,因此程序对应的状态机就像是下图这样:

如果做一个极端一些的假设,程序中所有的指令都是确定的,且由于状态空间是有限的,因此一定会形成 “循环”,即指令执行一段时间后,会到达一个已经经过的状态,然后继续周而复始执行。的确如此,你可以试着编写一个没有不确定性指令、没有系统调用、没有 undefined behavior 的程序,它将无法终止!

程序的不确定性的一个来源是 “不确定”的指令,例如,Intel 处理器提供了 rdrand 指令:

#include <stdio.h>
#include <stdint.h>

int main() {
  uint64_t val;
  asm volatile ("rdrand %0": "=r"(val));
  printf("rdrand returns %016lx\n", val);
}

将会生成一条 rdrand %rax 的汇编代码。如果用 gdb 调试,会发现每次程序运行,rax 寄存器都将被赋值为随机值,也就是在 rdrand 指令执行的状态,可能有多种不同的运行结果,状态机也在此产生了 $2^{64}$ 个 “分岔”:

另一个重要的不确定性指令是系统调用 (例如在 x86-64 上是 syscall 指令)。例如,_exit 系统调用将会销毁当前进程的执行,相当于从外界把状态机 “消灭”,进入一个 “不存在” 的状态。再比如 read 系统调用:

  1. 根据读入流的情况,有可能返回 -1 (失败)、0 (end of file)、某个正数代表读取的字节数;
  2. read 传入的 buf 可能会被操作系统修改为读取到的数据。

因此,根据当前调用 read 时物理设备、操作系统等的状态,read 系统调用可能的后续状态就更多了。

上面这个模型称为 “Simple Sequential Execution” (SSE),这对于我们理解计算机系统的执行是非常有帮助的——在我们的 NEMU PA 实验中,我们就模拟实现了你选择的指令集体系结构的 SSE 语义 (相当于 “抄了” 一遍手册)。

2.2. 并发程序的状态机模型

在课堂上,我们反复演示 (和强调) 并发程序的多个线程拥有独立的寄存器、堆栈 (但不同线程的堆栈位于同一个地址空间中,我们已经在课堂上展示过),共享代码和数据。因此并发程序的状态表示是刚才我们提到 $(M, R)$ 模型的一个自然扩展:系统中仍然有一份共享的内存,但每个线程都有独立的寄存器。因此假设系统中有 $n$ 个线程,那么状态看起来就是:

$(M, R_1, R_2, \ldots, R_n)$

注意到多线程程序 $(M, R_1, R_2, \ldots, R_n)$ 其实可以看成是若干个单线程程序。在任意时刻,状态的转换就是 “选择一个线程执行一条指令”:

也就是说,并发程序执行的每一步都是不确定的!并发程序的状态机模型如下图所示:

想要在实际的多线程程序上验证这个模型,我们不妨使用 pmap 命令打印一个多线程程序的地址空间映射:

$ ./hello-mt.out &
[1] 18401
$ pmap $!  # $! 是上一个后台进程的 pid
18401:   ./hello-mt.out
00005629379d2000      4K r-x-- hello-mt.out
0000562937bd2000      4K r---- hello-mt.out
0000562937bd3000      4K rw--- hello-mt.out
00005629387e7000    132K rw---   [ anon ]
00007fde98000000    132K rw---   [ anon ]
00007fde98021000  65404K -----   [ anon ]
00007fde9dd7c000      4K -----   [ anon ]
00007fde9dd7d000   8192K rw---   [ anon ]
00007fde9e57d000      4K -----   [ anon ]
00007fde9e57e000   8192K rw---   [ anon ]

如果在每个线程打印局部变量的地址,机会发现局部变量的确位于不同的 8192 KiB 内存映射区域,即我们假想的状态机模型的确符合操作系统上线程的实现。

动手实践

你可以试一试打印多线程程序每个线程局部变量的地址,并和 pmap 的结果对比,这将加深你对这个问题的认识,除此之外,在操作系统上实际编写一些程序,也能让你遇到一些只是学习理论未必会遇到的 “坑”,进一步增进你的理解——经验的积累使你的系统能力不断增长,不知不觉就会成为这一方面的专家。

事实上,将线程的堆栈放置在同一个地址空间中,在实现上既比较容易,同时对 C 程序的执行也是非常必要的,例如我们可以写出以下代码:

int *shared;

void thread1() {
  int x;
  ...
  shared = &x; // 局部变量的地址
  ...
}
void thread2() {
  ...
  *shared = 1; // 向另一个线程的堆栈中写入输入;
               // 只要 `thread1()` 不返回,这个写入就是合法的
  ...
}

这个模型帮我们更好地理解了什么是 “多线程程序”。所谓 “多线程程序是若干个共享内存的执行流”,不再是一个抽象、虚幻的概念,而是可以形式化地精确定义行为的数学对象。

$n$ 个线程的并发程序,若每个线程执行 $m$ 条指令,就算所有指令都是确定的,不同的执行顺序也多达 $n^{O(mn)}$,这根本就是个天文数字,也难怪并发程序的执行难理解了——冷不丁的犄角旮旯里就藏着并发的 bug。

2.3. 理解并发程序的执行

并发程序的状态机模型把并发程序的理解问题转换成了图论问题。在这里,我们举的是 Peterson 算法的例子——互联网上有大量的解释,因此我们在这里不再赘述。请大家跟随上课视频,画出 Peterson 算法的状态机,并证明它的正确性:

int turn, x = 0, y = 0;

void thread1() {
  [1] x = 1;
  [2] turn = T2;
  [3] while (y && turn == T2) ;
  [4] // critical section
  [5] x = 0;
}

void thread2() {
  [1] y = 1;
  [2] turn = T1;
  [3] while (x && turn == T1) ;
  [4] // critical section
  [5] y = 0;
}

思考题:为什么多此一举?

Peterson 算法中有三个变量,对应了现实中 $T_1$ 的旗子、$T_2$ 的旗子和一块牌子。这似乎是必不可少的——你可以试试如果只用旗子的互斥,例如:

void thread1() {
  x = 1;
  while (y);
}
void thread2() {
  y = 1;
  while (x);
}

上述代码将在两个人同时举旗之后陷入僵局。当然,你可以试着把旗子在举起后,如果观察到对方也举起旗子,就把自己的旗子放下:

void thread1() {
retry:
  x = 1;
  if (y) x = 0;
  if (!x) goto retry;
}
void thread2() {
retry:
  y = 1;
  if (x) y = 0;
  if (!y) goto retry;
}

但这将可能会陷入 “举起-放下” 的无限循环……(但其实这个算法已经足够好了)。

在共享内存上 (假设指令可以每次原子性地读取/写入一个变量) 实现线程的互斥困扰了学术界很多年,并在此基础上发展出了非常深刻的研究分支。有兴趣的同学可以选修秋季学期的《并发算法与理论》课程。

Peterson 算法 (以及其他并发算法) 的正确性分为两个部分:

2.3.1: 证明坏事永远不会发生 (Safety)

对 Peterson 算法来说,两个线程绝对不能同时进入临界区。线程进入临界区,意味着 $T_1$ 或 $T_2$ 进入了 $\textrm{PC}=4$ 的状态。所以 Peterson 算法满足 safety 的另一种表达是 “在任意程序的执行中,$\textrm{PC}_1 = 4 \land \textrm{PC}_2 = 4$ 不会出现”。

于是,对于任意的一个状态 $s = (M, R_1, R_2)$,我们都可以知道它是不是一个 “违反了 safety 的状态” (只需检查 $\textrm{PC}$ 即可)。从而,从初始状态出发,如果存在某个线程调度能达到一个 “坏” 的节点,我们就证明算法错了;否则算法就是正确的。

图论的语言和算法

把状态机看成是有向图 $G$,$G$ 满足 safety 当且仅当 $\textrm{PC}_1 = 3 \land \textrm{PC}_2 = 3$ 的节点在 $G$ 上不可达。假设我们已经构造了 $G$,这就图论中很基本的连通性问题 (通常是算法书上图论部分介绍的第一个算法),使用 dfs/bfs 可以轻松解决。

2.3.2: 证明好事永远会发生 (Liveness)

“好事总会发生” 的定义稍稍困难一些。我们将它表达为,“如果给两个线程足够的时间,一定至少有一个能进入临界区”,即到达 $\textrm{PC}_1 = 4 \lor \textrm{PC}_2 = 4$。

Liveness 定义的困难之处在于,我们要给 “两个线程足够的时间”。只给一个线程足够的时间是不够的——它自己可能无限循环,但只要让它和另一个线程交替执行几步,就可以进入临界区。

图论的语言和算法

把状态机看成是有向图 $G$,$G$ 满足 liveness 当且仅当不存在 $G$ 的一条 (无穷) 路径,在该路径上每个线程都执行了无穷多步,且所有经过的节点无一进入临界区 ($\textrm{PC}_1 \ne 4 \land \textrm{PC}_2 \ne 4$)。

“不存在” 性的证明通常求解它的反面:即我们只要求出一条不满足 liveness 的无穷路径,就能证明 liveness 被违反了。无穷路径怎么求呢?这里用一点算法上的小 trick:

  • 一条无穷长的路径、$T_1$, $T_2$ 都出现了无穷多次,当且仅当 $T_1$, $T_2$ 交替出现无穷多次。

换句话说,只要存在某个状态 $s$,从 $s$ 出发标有 $T_1$ 和 $T_2$ 的状态转换能够在有限步之内互相可达并回到 $s$ (且不进入临界区),且从初始状态 $s_0$ 到 $s$ 可以不进入临界区,我们就找到了一条满足条件的无穷路径。这可以用大家在图论中学过的 “强连通分量” 算法求解——这就是 Büchi Automata 的验证算法的核心之一。

“程序就是状态机” 是一个非常强大的工具,能够帮助我们理解程序的执行,这也是操作系统课程上所用为数不多的理论工具之一。

3. 实现一个 Model Checker

上述用图论的方法 “prove by brute-force” 在大家实际操作起来一定会遇到不小的麻烦——程序的执行非常 tedious,只要有一个地方有细微的小错,证明就可能不成立 (漏掉了可能出错的状态;或是得到了某个不可达的状态)。不过大家作为程序员,也立即会敏锐地发现:我们已经用数学的语言精确地描述了证明的方法,剩下的交给计算机不就好了吗?

3.1. 设计 Model Checker

没错,我们完全可以实现一个计算机程序 (Life is short, use python!) 来自动帮我们检查任何并发程序的正确性,例如在课堂上给出的参考 model checker 中,我们支持定义初始状态 (变量和它们的初值):

_init:
  x: 0
  y: 0
  turn: X

此外,我们需要给出每个线程执行的指令序列,其中每条指令 (每一行) 都必须是一行合法的 Python 代码,并且只能访问初始状态中定义过的变量 (对于每个线程的局部变量,我们可以在初始状态中定义每个线程的副本,例如 tmp_0, tmp_1)。此外,我们希望每一行代码都代表最小的 “一步” 执行,因此不能使用循环等复杂的结构。为了方便描述任何程序,我们在 Python 代码的基础上提供了额外的一个函数 GOTO,可以跳转到某条指令执行。

T1: |
  x = 1
  turn = 'T2'
  if y != 1: GOTO(4)
  if turn == 'T2': GOTO(2)
  x = 0
  GOTO(0)
T2: |
  y = 1
  turn = 'T1'
  if x != 1: GOTO(4)
  if turn == 'T1': GOTO(2)
  y = 0
  GOTO(0)

帮助我们检查正确性时,我们支持使用 Python 代码描述标记的条件。这里可以使用 PC: dict,可以从线程名中取出当前执行指令的位置。

_bug_on: |
  PC['T1'] == 4 and PC['T2'] == 4 # 在两个线程同时进入临界区时标记错误
_mark_on: |
  PC['T1'] == 4 or PC['T2'] == 4  # 在至少有一个线程进入临界区时标记提醒

3.2. 实现 Model Checker

大家可能感到意外,model checker 的实现异常简单,它的核心是一个大家熟悉的 breadth-first search 的循环,再熟悉不过的代码:从队列中取出头部的元素,然后枚举线程、执行一步 (expand),如果得到的状态未被访问过,就添加到队列中。最后我们得到 nodesedges 组成的状态图:

queue, explored, nodes, edges = [ s0 ], { H(s0) }, [ s0 ], []
while queue:
  s, queue = queue[0], queue[1:]
  for t in threads:
    s1 = expand(s, t)
    if H(s1) not in explored:
      nodes.append(s1)
      queue.append(s1)
      explored.add(H(s1))
    edges.append((H(s), H(s1), t))

Model checker 实现中第一个有趣的 hack 是我们对代码的预处理。Python 中并没有 GOTO——我们是如何表达线程状态 (PC) 的变化的呢?短短几行的程序:

def parse(code):
  for line in code.strip().splitlines():
    yield re.sub(r'GOTO\((.*?)\)', r'pc = \1 - 1', line.strip() + '\npc += 1')

会把 GOTO(x) 替换成 pc = x - 1,并且在每条指令之后都增加一行 pc += 1。所以,我们的指令序列,例如 Peterson 算法中的 turn = 'T2' 会被替换为

turn = 'T2'
pc += 1

if y != 1: GOTO(4) 则会被替换为

if y != 1: pc = 4 - 1
pc += 1 # 因为 pc += 1 是每次都添加的,所以 GOTO 的目标减去了 1

在此基础上,我们又用了 Python 可以在运行时执行任意代码的特性,实现了非常简洁的 expand:

def expand(s, t):
  pc   = s['PC'][t]
  stmt = P[t][pc]
  s1   = { **s, 'PC': s['PC'].copy(), 'pc': pc }
  exec(stmt, {}, s1) # hah! we're cheating!
  s1['PC'][t] = s1['pc']
  return { k: s1[k] for k in variables }

在状态 s 中,除了包含变量的值 (x, y, turn) 之外,还有 PC 保存了每个线程的执行位置。我们首先把当前执行线程的 PC 提取到 pc 变量中 (pc = s['PC'][t]),然后执行代码,最后把 pc 写回到 s1['PC'][t] 中,就完成了一步状态的扩展。

大家可以自由修改 model checker 的代码,以使它们的使用更顺手,例如我们可以仅在发现新节点时才加入边到 edges,从而能得到树结构的状态,更易于阅读:

Peterson 算法的状态树,只显示到达每个状态的最短路径树。

4. 延伸阅读

我们在上课时,介绍了如何用状态机模型理解 time-travel debugging 和 record & replay。这两个计算机系统领域的 “黑科技” 在状态机意义下的解释非常清楚明确:

在有了状态机的视角之后,我们就有了具体实现这些技术的切入点。例如,如果我们希望在调试器上实现 time-travel debugging,我们只需要在单步模式下分析当前 PC 指针下的指令,解析出该指令所有可能产生的副作用,并予以记录——事实上,gdb 的确就是这么实现的。

再例如,如果我们要实现 record & replay,一个重要的问题是如何 “拦截” 那些具有不确定性的指令。通过查阅资料 (互联网、论文、文档),我们一方面可以使用 ptrace 系统调用,或使用编译器提供的接口拦截指定的函数调用,另一方面也可以通过修改程序的二进制代码 (例如像 gdb 一样给有不确定性的指令打补丁),使有不确定性的指令执行时跳转到指定位置的代码。

计算机系统里没有什么 “魔法”——计算机系统就是一个状态机。哪怕是最顶尖的研究成果,也是在这个框架下完成的,例如从状态机上的一次执行 (即测试输入决定的一条路径) 出发,通过改变一个分支的方向 (并保持之前的分支不变),以求解出更多的测试用例覆盖更多的代码。

在 trivial model checker 中,我们使用了队列和集合来存储探索过的程序状态——这种技术称为 “stateful” 的 model checking。但你一定也好奇:如果我们想 model check 实际中的程序,而程序中有太多的变量,如果直接将它们放在状态中,那状态空间就太复杂,算法肯定执行不完了。是否有可能像 “走迷宫” 那样,不记录走过的状态,但又可以有效地探索状态空间?

最后给大家一个思考题:是否能在在并发程序上实现 time-travel debugging 或 record and replay?因为并发多线程的调度 (指令的执行顺序) 是重要的不确定性来源,因此想要再时间上回溯或是重放执行,就必须把因线程调度导致的不确定性记录下来——例如,记录所有共享内存访问的顺序。这是一个非常有挑战性的问题,jyy 的博士论文就在这方面做了一些理论和实际的工作——甚至提出了一个有些悲观的猜想 (做了部分情况的证明):在没有硬件机制的帮助下,如果想观测/记录并发程序的执行,我们要么不可避免地在程序里增加同步操作,要么就要在重放时付出 NP-Completeness 的代价。

Creative Commons License    苏 ICP 备 2020049101 号