关注同步(synchronization)所需要的设施。
consensus: an elementary synchronization problem
consensus object: decide(), called at most once
consensus protocol: wait-free consensus implementation
并发地调用 decide() 可以线性化成顺序调用 decide() 其中被选中的线程是最先完成 decide() 的。
move: 调用一次共享对象的方法
protocol state: 线程和共享对象的状态(如果各线程自己的执行序列一样,对 shared object 的修改彼此独立,没有先后关系(比如各自修改不同的位置),那么就可以认为是同一个 protocol state)
initial state: 线程没有 move 时的 protocol state
final state: 所有线程结束时的 protocol state
decision value: 决定的值,在 binary consensus 中就是 0 或者 1.
bivalent: 二阶的,修饰 protocol state, 表示其还不能决定 decision value (当前既可能是 0 也可能是 1)
univalent: 一阶的,修饰 protocol state, 表示当前已经能决定 decision value.
对 Lemma 5.1.1 证明的理解:一个线程 decide() 只会按照自己已知的信息进行判断。 如果一个线程在其他线程调用 decide() 之前完成 decide(),那么知道的信息只有自己的 input,必然 decide 出自己 input 的值。 之后的线程也要服从这个结果。至于能不能确实地服从,以及第一名会不会出现矛盾,就是 consensus protocol 正确性的关键了。 这个证明本身是一个构造性证明,用两个极端的例子指出开始既可能 decide 出 0 也可能 decide 出 1.
critical state: bivalent, 一 move 就 univalent. 也即是 decide 的分歧点。
A runs solo: 线程 A 独自跑完全程。
Theorem 5.2.1 的证明思路是从 critical state 开始,设定 B 独自跑完全程,从其应然中构造矛盾。
所以要对 A 的情况进行讨论。A 在 cs 处读的话,改变了 decide 的走向,然而 A 并没有真地修改 shared object,
但是 B 跑完全程就和直接跑全程不一样了,矛盾(
或者说,在 cs 处能否允许这样一个没有实质影响的 move?也就是只读 move 能否让 bivalent 降到 univalent?
非也,首先执行有多种线性历史,由此构造出树,显然存在刚好在只读 move 前生成 critical state 的情况,这是由结构而非语义决定的。)。
在 critical state 后,两个子树不能出现相同的 state,否则矛盾。
至于写同一个 reg 的情况,因为 run solo 的线程都是后执行的,所以覆盖了它自己也就分不出来了,产生矛盾。
重要启示:计算机要想同步,硬件必须提供额外的同步原语。
这一节其实是借上一节 consensus 的结论来证明: 不能从 atomic register 构建多入队/出队的 FIFO 队列。 (如果可以的话,就能用 atomic register 构建 2-concensus 了)
Definition 5.1.1 class C solves n-thread consensus 的定义
Definition 5.1.2 consensus number
Corollary 5.1.1 solve n-thread consensus 的传递性
Lemma 5.1.1 2-thread consensus protocol 初态 bivalent
Lemma 5.1.2 n-thread consensus protocol 初态 bivalent
Lemma 5.1.3 wait-free consensus protocol has a critical state
Theorem 5.2.1 atomic register's consensus number = 1
Corollary 5.2.1 仅仅 atomic registers 不能胜任 consensus number > 1 的场合。
Theorem 5.4.1 二出队 FIFO 的 concensus number >= 2