My Avatar

JacketWoo

King Birds Fly Fast and Early!

FLP 证明

2018年04月28日 星期六, 发表于 北京

如果您对本文有任何的建议或者疑问, 可以给我发邮件(seuxfw1990@gmail.com)或者在 这里给我提 Issues, 谢谢! :)

最近有点空闲时间,就将以前的看过的FLP论文,又重新温习了一遍,为了便于以后可以快速回顾,所以记下这篇笔记

FLP论文 由Fischer, Lynch 和 Patterson三位分布式领域大牛于1985年发表,论文要表达的主题是:分布式异步模型中,没有一种一致性协议可以保证系统在某个进程(服务)挂掉后仍然是完全可靠的。

一些概念

  1. 分布式异步网络模型

    a. 每个步骤的处理速度是未知的,可以很快,也可以很慢;

    b. 消息在进程之间的传递速度也是未知的;

    c. 进程内部或者之间,没有同步时间可以使用(这意味着没有办法使用超时等机制)

    ……

    基于以上几点,还可以推导出: 进程间没有办法判断出对方是否存活等

  2. 一致性协议系统

    一致性协议系统P: 由N(N>=2)个进程以及它们共有的一个消息队列组成

    每个进程:由输入{可以为0,1},转换函数、输出{可以为b,0,1}组成

    ​ 输出一旦确定后,则无法更改

    通信队列:存储已经发送,但是还没有被接收的消息

    ​ 不保证消息的投递顺序和速度

    ​ 如果消息的目标进程是正常的,保证最终可以将消息投递到对应的进程(可能投递/进程接收了很多次)

    一致性协议系统的状态C:每个进程的内部状态和通信队列的状态共同组成了整个一致性协议系统P的状态

    step: 某个状态到下一个状态的过程,一般分为两步:a) 某个进程从通信队列内接受消息;b) 针对接收到的消息进行处理,并可能向其他进程发送消息。

    e(p, m):用于标记p进程接收到消息m对应的step

    run:一串step称为一个run,记为σ

    σ(C):代表状态C在进过σ后的状态

    P的初始状态:各进程的初始状态{输入x(不确定),转换函数(确定),输出(确定,为b)} 和 空的通信队列

    可到达状态: 若C1=σ(C0),则称C0到C1是到可达(reachable)的

    可访问状态: 将从初始状态可达的状态都称为可访问(accessible)的

    进程正常:代表可以执行无限次的step(不断的从通信队列中获取消息,没有的话,就获取到空消息),否则不正常

    admissible run:在该run内,最多只有一个进程不正常工作,并且所有发送到正常工作进行的消息最终都被接收到了

    deciding run:在该run内,有进程到达了决议状态(输出为确定值)

    ··············································································································

    确定的状态:如果某状态下,有进程的输出为决议值,则称该状态具有决议值

    部分正确的一致性协议:满足 a) 任何一个状态的决议值数量小于等于1;b) 对于任何一个0或者1的决议值v,都决议值为v的可访问状态。

    完全正确的一致性协议: a) 部分正确;b) 每一个admissible run都是deciding run

    ··············································································································

    令V为从C开始的所有可达状态的决定值的集合,则:

    bivalent: V元素数量为2

    univalent: V元素数量为1

    0-valent: 在V元素数量为1的情况下,元素之为0,对应的状态称为0价的

    1-valent: 与0-valent相对应

    备注:根据“部分正确”的定义,可以推出,i-valent的状态及其之后所有的可达状态都是i-valent的

证明

“完全正确一致性协议”的定义比较严格,要求每个adminssible run都是deciding run,这个有些不太现实,我们通常的工程实践中,一般的要求是“任何一个无限长的adminssible run都是deciding run”,即要求每个无限长admissbile run内的某些有限长run,可以使一致性协议系统P达到决议状态。

论文也是按照“存在这样的一个无限长的admissible run,使得一致性协议系统P达不到决议状态”这个思路来证明“没有一种一致性协议可以保证系统在某个进程(服务)挂掉后仍然是完全可靠”,这种证明方法对我们的项目实践更加具有指导意义。

引理一:交换性

1
Suppose that from some configuration C, the schedules ul, (~2lead to configurations C1, C2, respectively. If the sets of processes taking steps in c1 and 02, respectively, are disjoint, then u2 can be applied to Cl and (~1can be applied to C2,and both lead to the same configuration C,. (SeeFigure 1.)

证明:这个比较简单,就不细述了。

备注:但是我觉得,这里可以交换的两个步骤串,应该没有逻辑上的因果关系,如其中一个步骤串是基于另外一个步骤串产生的,否则交换性引理是否成立就需要进一步深究了。

引理二:

1
P has a bivalent initial configuration.

证明:采用反证法。假设P的初始状态都是univalent的。

​ P的所有的初始状态应该只有各个进程的输入不同,将相邻的输入不同放在一起,按照这种顺序排成一个环。基于我们的假设和“部分正确”的定义,可以直观的推导出,存在两个初始状态C0(决议值为0)和C1(决议值为1),只有进程p的输入Xp不同,但是它们分别是0-valent和1-valent的。

​ 假设进程p是不正常工作的,则任意一个步骤串σ,σ(C0)和σ(C1)应该只有p的内部状态不同,它们应该具有相同的决议值。如过该决议值为0,C1是bivalent的;若该决议值为1,则C0是bivalent的。与假设矛盾,假设不成立。引理证明完毕

引理三:

1
Let C be abivalentconfigurationofP,and let e = (p, m) beanevent that is applicable to C. Let Cc be the set of configurations reachablefrom C without applying e, and let Dd = e(Cc) = {e(E) | E ∈ Cc and e is applicable to E}. Then, Dd contains a bivalent configuration.

证明:同样用反证法。假设Dd内的状态都是univalent的。

​ 可以简单的推导出存在Cc内存在这样的两个两个状态C0和C1,C1=e’(C0),满足D0=e(C0)是0-valent的,D1=e(C1)是1-valent的。

可以这么理解这里的“简单推导”:1)Dd中总共包含的决议值有两个,这个是由部分正确的定义推导出来的;2)从初始状态C(0)开始,第一步骤就执行e,如果得到的状态为0-valent的,若第一个步骤执行其他的操作,然后第二个步骤执行e,得到1-valent的状态,则满足要求;如果第二个步骤是e,执行后的状态还是0-valent,那就看到第三个步骤是e后的状态,依次类推,总会有一个状态,在执行e后,变为1-valent的

​ 记e’ = (p’, m’)。如果:

​ 1) p’ != p,则根据引理1,可得

flp-figure2

e’(D0) = D1,矛盾了;

​ 2)p’ == p,依据交换性,依然可以得到:

flp-figure2

图中,σ是一个不包含p的deciding run(根据某个进程不正常工作后,仍然”完全正确”的定义,存在这样的一个run)。显然也得出了矛盾,因为σ是deciding run,所以σ(C0)是univalent;而从A又可达E0和E1,则说明A是bivalent,所以矛盾。

​ 综合起来,假设不成立。引理3得证

定理一:

1
No consensus protocol is totally correct in spite of onefault.

证明:按照之前说的,可以证明没有“partially correct”,来间接的证明没有“totally correct”。论文中是通过设想存在一个无限长,但却始终得不到决议值的run,来证明这一点。

​ 设想有一个进程队列(初始的时候,进程队列的各个进程可以随机排列),在执行一致性协议过程中,当进程队列的排头进程p接收到消息并处理后,则将它排到进程队列的尾部。并且将这个时候,标记为一个旧阶段(stage)的终结和一个新阶段的开始。这样所有的run都可以被分为这样的有限个或者无限个阶段了。

​ 假设P的初始状态是bivalent的,根据引理3,可以推导出,对于每个阶段,都存在这样的步骤串,使得该阶段结束的状态仍然是bivalent的。从而使得这个一致性协议系统永远无法达到决议状态。

​ 定理一得证。

定理一的证明过程中,有两个地方用到了”一个进程不正常工作“的条件,a) 引理二的证明,这个是初始状态就确定了的;b) 引理三的证明过程,p == p’情况下存在一个不包含p的deciding run的使得 A=σ(C0)的条件,这个是可以在一致性协议执行过程中出现的。

定理二:

1
2
There is a partially correct consensusprotocol in which all non- faulty processes always reach a decision, provided no processes die during its
execution and a strict majority of the processesare alive initially.

证明:论文中对这个定理的证明,是通过提供一个满足要求的协议算法来实现的。该协议分为两个阶段:

第一阶段:每个进程向其他进程广播自己进程编号,然后等待接收ceil((N+1)/2)-1个回应(每个回应记为{i, j},从i到j的回应);

第二阶段:每个进程在第一阶段后,向其他进程广播自己接收到的L-1个回应的信息。这个阶段,每个进程都会根据接收到的信息,建立传递闭包G+。对于每个接收进程来说,当它接收到所有知道的(包括第一阶段感知到的和第二阶段感知到的)其他进程在第二阶段广播的消息时,它的接收过程结束。

第二阶段结束后,每个进程都会得到一个G+,因为假设协议执行过程中是没有进程挂掉的,所以根据约束,各个进程在第二阶段结束后会得到相同的G+,然后在G+上确立一个“initial clique”,该“initial clique”的特征为:1) 没有任何来自该“initial clique”之外的其他节点的输入;2) 该initial clique的内每个节点也是它每个“祖先”节点的“祖先”。因为该“initial clique”元素数量至少大于L,所以G+内只存在一个这样的“initial clique”

依据假设可以得到,所有正常工作的进程最终都会完成第二阶段。每个完成第二阶段的进程,在确定的“initial clique”上,按照转换函数,确定输出值。因为所有正常工作进程上的“initial clique”都一样,所以,所有正常工作进程上的输出值也一样,一致性协议工作完成。

因为存在这样一个协议,所以定理二得证。