第六讲 并发控制基础

Peterson算法、模型检验和软件自动化工具

主要内容：

如何阅读理解教科书、互联网上的各种并发程序

如何保证互斥：一个很简单的例子Peterson算法

以及如何画出并发程序状态机的状态

如何保证一个全局变量某一刻只被一个线程写、读？

<=>如何保证一个厕所某一刻只被一个人使用？

Peterson算法

A和B争抢厕所，但是他们都很谦让。

上厕所前，需要事先举旗并贴字。具体来说

  • 如果A想要上厕所，会事先举起旗子，旗子上写了A，并且将厕所门口贴上B
  • 如果B想要上厕所，会事先举起旗子，旗子上写了B，并且将厕所门口贴上A

准备工作做好以后，下一步将根据旗子和厕所门口的字来决定是否进入厕所。具体来说

  • 如果A想要进入厕所，会观察是否有人举起旗子，如果B举了旗子，且门上的贴了B，他将等待，否则A将进入厕所
  • 如果B想要进入厕所，会观察是否有人举起旗子，如果A举了旗子，且门上的贴了A，他将等待，否则B将进入厕所

出厕所后，将放下自己的旗子。

这种奇怪的算法将保证A或B进入厕所时，厕所没人。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

#include "thread.h"

#define A 1
#define B 2

atomic_int nested;
atomic_long count;

void critical_section() {
  long cnt = atomic_fetch_add(&count, 1);
  assert(atomic_fetch_add(&nested, 1) == 0);
  atomic_fetch_add(&nested, -1);
}

int volatile x = 0, y = 0, turn = A;

void TA() {
    while (1) {
/* PC=1 */  x = 1;
/* PC=2 */  turn = B;
/* PC=3 */  while (y && turn == B) ;
            critical_section();
/* PC=4 */  x = 0;
    }
}

void TB() {
  while (1) {
/* PC=1 */  y = 1;
/* PC=2 */  turn = A;
/* PC=3 */  while (x && turn == A) ;
            critical_section();
/* PC=4 */  y = 0;
  }
}

int main() {
  create(TA);
  create(TB);
}

我们会不自觉地提出一些问题：

  • 如果结束后把门上的字条撕掉，算法还正确吗？
    • 在放下旗子之前撕
    • 在放下旗子之后撕
  • 如果先贴标签再举旗，算法还正确吗？
  • 我们有两个 “查看” 的操作
    • 看对方的旗有没有举起来
    • 看门上的贴纸是不是自己
    • 这两个操作的顺序影响算法的正确性吗？
  • 是否存在 “两个人谁都无法进入临界区” (liveness)、“对某一方不公平” (fairness) 等行为？
    • 都转换成图 (状态空间) 上的遍历问题了！

为了保证peterson的正确性，我们还需要什么？

  • 原子指令来保证读/写单个变量是“原子不可分割”的
  • 编译器设置屏障

当然这种奇怪算法的正确性需要验证，接下来的所有内容都是围绕验证的。

一种方法是通过人脑来枚举A和B抢着上厕所以及举旗过程的所有状态。模拟多线程执行代码的顺序。

另一种方法是计算机验证，jyy的功底就体现出来了。

使用Python这种动态语言模拟验证状态机正确性。 Model checker

并利用某些库可视化状态机的所有状态。

jyy利用了Generator的一个特性来保存函数运行的上下文。这使得我们能够更方便地模拟状态机的执行过程。

关于Model Checker的Python实现和可视化展示这里就暂且不说了。

所以究竟是怎么做到的，还需要看看2022年的视频

这节课告诉了我们工具的重要性，计算机辅助验证彳亍，人脑模拟计算机不彳亍！