Skip to content

Instantly share code, notes, and snippets.

@Wonicon
Created November 2, 2017 17:49
Show Gist options
  • Save Wonicon/db6418cbe61a611c0ff2e9085a90ca92 to your computer and use it in GitHub Desktop.
Save Wonicon/db6418cbe61a611c0ff2e9085a90ca92 to your computer and use it in GitHub Desktop.
Art of Multiprocessor Notes

CH.5

关注同步(synchronization)所需要的设施。

5.1

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 的分歧点。

5.2

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 的线程都是后执行的,所以覆盖了它自己也就分不出来了,产生矛盾。

重要启示:计算机要想同步,硬件必须提供额外的同步原语。

5.4

这一节其实是借上一节 consensus 的结论来证明: 不能从 atomic register 构建多入队/出队的 FIFO 队列。 (如果可以的话,就能用 atomic register 构建 2-concensus 了)

5.5

定义索引

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment