八月份已经过去了，放假前立下的 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 而言
- 举手
- 等待 Bob 放手
- 放宠物进花园
- 等宠物回来
- 放手
对 Bob 而言
- 举手
- 看 Alice，如果 Alice 举手就放手，等待 Alice 放手后再举手
- 放宠物进花园
- 等宠物回来
- 放手
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}\)
实际上并行处理是存在通信和同步开销的，这会反映在时间花费上。