TAOMP01 Intro
2022-09-01 16:33:49

八月份已经过去了,放假前立下的 flag 还有好多没有实现...

但是这本是上学期上 OS 就想看的书,更早是在吃土耳其烤肉的时候就被安利过

开干吧...

Intro

why multiprocessor

摩尔定律失效,现代的 CPU 已经引入了多核架构,现代的程序设计也在拥抱并行来提升性能

what's different

多个并发的执行流操作若干共享的对象是一种常见的并发计算模型,在这之上会遇到

  • 正确性的问题,计算模型的变化使得原本正确的程序变得不正确
  • 性能的问题,对共享对象的操作需要某种“序列化”
  • 能力的问题,并非所有单线程程序都可以“改造”成多线程
  • 评估的问题,我们应当如何评价一个多线程程序的优劣?

what's in interest

  • liveness property,即并发的系统不会卡住。例如 deadlock-freedom
  • safety property,即并发的系统不会进入某些错误状态。例如 mutual exclusion

Shared states

又是那个经典的多线程共享 Counter 的栗子

一句话解释:单线程计算模型下的编程语言没有提供语句的原子性保证,这一历史包袱导致了共享状态在多线程下需要做同步操作。

解决办法是人为地打包捆绑某些指令,规定这些“指令包”是原子的。这样的性质(某段代码/某个对象 在同一时刻只能有一个线程执行/访问/修改)被称为 mutual exclusion。当然也可以叫做某种“协议”,指的是多个并发的执行流通过某种约定好的方式访问这些共享对象。

栗子

描述

Alice 和 Bob 各自养了宠物,他们共享一个花园。要求宠物不能同时出现在花园中,且两人的宠物都有进入花园的机会,要设计一个通信协议。他们各自可以举手,也可以看到对方有没有举手,除此之外没有别的交流手段。

协议

对 Alice 而言

  1. 举手
  2. 等待 Bob 放手
  3. 放宠物进花园
  4. 等宠物回来
  5. 放手

对 Bob 而言

  1. 举手
  2. 看 Alice,如果 Alice 举手就放手,等待 Alice 放手后再举手
  3. 放宠物进花园
  4. 等宠物回来
  5. 放手

mutual exclusion

假设存在某个时刻两人的宠物都进了花园,分别考虑两人的最后一次通信流程:

由 Alice 放了宠物可知,此前Alice 必然举起了手、看到了 Bob 放手。因此 Bob 最后一次举手必然发生在 Alice 最后一次看之后,这说明 Bob 必然能看到 Alice 举起了手。

由 Bob 放了宠物可知,此前Bob 必然举起了手、看到了 Alice 放手。这就产生了矛盾,故假设不成立。

deadlock-free

证明是类似的

starvation-free

是不满足的,例如当 Alice 和 Bob 总是同时举手时,Alice 的宠物总是优先进花园。

fault-tolerance

某一方可能出错,这时候另一方需要等待出错方恢复正常。

一些分布式的协议则会有专门的询问/验证环节来容忍节点的错误甚至是离线

Pattern

可以发现类似的证明通常只关心若干时间之间的拓扑关系,通过协议来限制事件发生的顺序成为我们想要的形状。

这样也就能理解为什么后面要抽象出 DAG 的证明模型了。

Back to CS

  • 这种基于 举手/看 的通信协议本质上是延时的,即双方不需要约定时间后建立连接
  • 举手/看 分别代表原子的 写/读 操作,并且各自只占据一个比特

Producer-Consumer

这个就不写了。

producer-consumer

这个性质说的是两个/两类线程满足

  • 一类读取共享缓冲区 当且仅当缓冲区已满
  • 一类写入共享缓冲区 当且仅当缓冲区为空

Pattern

涉及到状态存储的协议,就可以用探索状态的方式来证明正确性了。即“某协议保证XX不会出现”当且仅当“在任意合法的状态上XX都不成立”。而这又可以用 初始状态满足性质P + 状态转移保持性质P 这个套路来证明。

Reader-Writer

这个也不写了

Amdahl’s law

一个简单的公式,含义为:我们如果能使得 \(p\) 的任务加速 \(n\) 倍(通过 \(n\) 个核心),那么得到的效率增长是 \(S\)\[ S=\frac{1}{(1-p)+\dfrac{p}{n}} \] 可以发现当 \(n\to \infty\) 时,\(S\to \dfrac{1}{1-p}\)

实际上并行处理是存在通信和同步开销的,这会反映在时间花费上。