1. FLP impossibility背景
FLP Impossibility(FLP不可能性)是分布式领域中一个非常著名的结果,该结果在专业领域被称为“定理”,其地位之高可见一斑。该定理的论文是由Fischer, Lynch and Patterson三位作者于1985年发表,之后该论文毫无疑问得获得了Dijkstra奖。
顺便要提一句的是,Lynch是一位非常著名的分布式领域的女性科学家,研究遍布分布式的方方面面,对分布式领域有着极其卓越的贡献,其著有<<Distributed Algorithms>>一书,书中有非常严谨而简洁的逻辑讨论了许许多多的分布式算法。
FLP给出了一个令人吃惊的结论:在异步通信场景,即使只有一个进程失败,也没有任何算法能保证非失败进程达到一致性!
因为同步通信中的一致性被证明是可以达到的,因此在之前一直有人尝试各种算法解决以异步环境的一致性问题,有个FLP的结果,这样的尝试终于有了答案。
FLP证明最难理解的是没有一个直观的sample,所有提到FLP的资料中也基本都回避了sample的要求。究其原因,sample难以设计,除非你先设计几种一致性算法,并用FLP说明这些算法都是错误的。
2. 系统模型
任何分布式算法或定理,都尤其对系统场景的假设,这称为系统模型。FLP基于下面几点假设:
- 异步通信
与同步通信的最大区别是没有时钟、不能时间同步、不能使用超时、不能探测失败、消息可任意延迟、消息可乱序 - 通信健壮
只要进程非失败,消息虽会被无限延迟,但最终会被送达;并且消息仅会被送达一次(无重复) - fail-stop模型
进程失败如同宕机,不再处理任何消息。相对Byzantine模型,不会产生错误消息 - 失败进程数量
最多一个进程失败
- Termination(终止性)
非失败进程最终可以做出选择 - Agreement(一致性)
所有的进程必须做出相同的决议 - Validity(合法性)
进程的决议值,必须是其他进程提交的请求值
3. 一个Sample
4. Paxos为什么可以?
其实仔细回忆Paxos论文会发现,Paxos中存在活锁,理论上的活锁会导致Paxos算法无法满足Termination属性,也就不算一个正确的一致性算法。Lamport在自己的论文中也提到“FLP结果表明,不存在完全满足一致性的异步算法...",因此他建议通过Leader来代替Paxos中的Proposer,而Leader则通过随机或其他方式来选定(Paxos中假如随机过程会极大降低FLP发生的概率)。也就是说Paxos算法其实也不算理论上完全正确的,只是在工程实现中避免了一些理论上存在的问题。但这丝毫不影响Paxos的伟大性!
5.定理证明
5.1 一些定义
- 消息队列:
假定存在一个全局的消息队列,进程可以发送消息,也可以在其上接收消息。
send/receive:send(p,m)是指给进程p发送消息m,只是放入队列,称”发送“,如果消息被p接收,成送达(delivery);receive(p):接收发送给p的消息,若没有则返回空
消息队列实际上是模拟了异步通信,即消息会被延迟、乱序 - Configuration:前面已经提到,所有进程的状态集合,进程的状态包括初始值、决议值、消息队列的内容
初始Configuration:各个进程初始值是随机的、消息队列为空、决议为空的开始状态 - 事件e=(p,m)
事件代表给某个进程发送消息,并且消息已经送达。正是因为执行了某个事件,导致Configuration变化为另一个Configuration - 事件序列run
一连串顺序执行的事件序列称为一个run - 可达Configuration
如果某个Configuration A执行了一个run得到另一个Configuration B,则称B从A可达
5.2 引理1(连通性)
【把所有的进程P分成两个不相交的集合P1,P2,有两个run R1,R2,如果先给P1应用R1,再给P2应用R2与先给P2应用R2,再给P1应用R1,对P的Configuration C来说得到的结果是一致的(结果显而易见,不再罗列证明)】
5.3 引理2(初始Configuration不确定性)
5.4 引理3(不可终止性)
5.4.1 证明的正规化
5.4.2 证明D中既包含决议为”提交“的Configuration,也包含决议为”回滚“的Configuration。也即证明D中的Configuration不是单值决议。
5.4.3 若D是”确定“的,则导出一个矛盾
6. 总结
7. 参考资料
- Impossibility of Distributed Consensus with One Faulty Process
- http://the-paper-trail.org/blog/a-brief-tour-of-flp-impossibility/comment-page-1/#comment-102212
- Lynch的大作:<<Distributed Algorithms>>
- FLP_and_Paxos.pdf(Ken Birman)
- Ken Birman教书的网站:http://www.cs.cornell.edu/ken/
Origin
在处理和分析数据时,最理想的环境是这样的:一台有无限存储和计算能力的“超级计算机”,可以提供无穷大的存储容量,并且可以将计算时间降低至无穷小。
《银河系漫游指南》中全宇宙全时空第二强的计算机“深思”,花费750万年时间,计算出了“宇宙、生命及万物 ”终极问题的答案:42
这样一台“超级计算机”在现实世界中并不存在。计算机的存储和计算能力始终要受到客观物理规律的限制。在可预见的将来,单位存储单元上无法存储超量的数据;而在运行计算任务时,由于芯片计算能力是有限的,当计算需求超过瞬时计算能力时,往往会发生排队现象。为了解决大量数据的存储和计算能力不足的问题,我们有两种选择:
1.纵向扩展
即升级硬件设备。通过如升级存储量更高的硬盘、单位时间运算速度更高的芯片,可以为计算机提升性能和存储量,来解决上述问题。但这种硬件的升级会受到计算机本身架构的局限,同时进一步升级所需要的成本会快速上升,从而使得升级硬件的边际效益快速下降。此外,升级所用的硬件依然具有其自身的局限性,并不能彻底解决上述的问题。
2.横向扩展
使用多台普通计算机来模拟“超级计算机”。也就是使用多台机器各自并行地进行存储和计算这种方式进行模拟。使用这种方式构建的计算机系统叫做分布式系统,它具有以下三个特点:一组计算机、通过网络传递信息、协调计算机的行为。通过这种方式,我们可以近似地获得无限的存储和计算能力,解决单机下存储和计算的局限。
作为通过网络连接的多台计算机系统,分布式系统的设计目标一般包括:
扩展性 :增加机器不改变或极少改变系统行为,并能获得近似线性的性能提升;
性能 :指分布式系统进行服务时的延时和吞吐率是满足用户需要的;
可用性 :分布式系统的核心需求,表示分布式系统是否处于整体可服务并且一直可服务的状态;
容错性 :系统发生错误时,系统有对错误进行规避和恢复的能力。
通过搭建合理的系统架构,进行恰当的数据管理,分布式系统是可以满足以上的设计目标的。一套顺畅运行的分布式系统可以在很大程度上满足大量数据的存储和计算需求。尽管如此,任何事情都需要付出代价。分布式的方式不仅增加了工程复杂性,甚至在理论上会出现不可逾越的障碍。本文将根据GeneDock的分布式实践经验对这些优缺点进行必要的探讨。
Problem
为了实现分布式系统的设计目标,我们需要先了解分布式系统实现过程中需要克服的问题和困难。一套分布式系统的主要物理要素包括节点的数目以及节点间的距离。仅这两点的更改就会引入以下限制:
节点数增加会导致系统整体出错概率增大
节点数增加会导致节点间通信量增加
节点间距离增加会导致系统最优(或部分)性能变差
抛开工程的视角,仅从理论层面看,分布式系统也存在着如下三类视角的系统划分:
保持一致 :系统中相关数据间的逻辑关系应当是正确和完整的。极端情况下,从系统中任意部分读取而获得的数据应当都为最近写入的数据;
处理失效 :分布式系统可能出现的失效状况有三类:节点失效、网络分区失效、拜占庭失效。极端情况下,系统的执行和操作不会受到任何系统内部失效的影响;
时钟同步 :分布式系统有两种模型:同步系统和异步系统。同步系统会确保所有执行过程的步调一致,且各执行过程有精确的时钟。即任意处理过程能够得到精确的执行流程的偏序关系,也就意味着每个处理过程和通信都在有限的时间内进行。异步系统则相反,没有任何时序性保证。即各处理过程是完全以自己的节拍在运行,不存在有效的同步时钟,也意味着过程间的通信延时可能会趋于无穷大。
针对物理层面和理论层面存在的种种问题,分布式系统研究人员希望找到这些问题的答案:是否可以通过硬件技术和软件算法来克服困难,实现一个理想的或接近理想的分布式系统,以达成模拟那台“超级计算机”的设计目标?
Impossibility
不幸的是,在实际应用中,理想的分布式系统实际是不可能实现的。
图为历史上最著名的第一类永动机“魔轮”。人类花费超过500年的时间才学习到:Something is impossible.
P.S. “中华宇宙能源超磁能机车”——即使在永动机历史上也是非常“出彩”的。可以去百度永动机贴吧长长见识 (╯□╰)
为什么?我们可以从一致性问题(Consensus Problem)——也就是分布式系统必须解决的一个问题出发,同时考虑其他设计目标,看看可以推导得到什么样的结果。一致性问题(Consensus Problem)是指:
一致(Agreement) :每个正确的执行过程应该在相同的值上达成一致;
完整(Integrity) :每个正确的执行过程最多只能决定一个值。如果它决定了某个值的话,这个值一定是被某个执行过程提出的;
终止(Termination) :所有的执行过程最终会做出一个决定;
正确(Validity) :如果所有正确的执行过程提出了相同的值V,那么所有正确的执行过程都会决定值V。
基于以上要求,可以推导出在分布式系统领域非常重要的定理:
FLP不可能性在假设网络可靠、计算节点只会因崩溃而失效的最小化异步模型系统中,仍然不存在一个可以解决一致性问题的确定性算法。
仅这一条定理就已经打碎了我们模拟“超级计算机”的幻想。不过从务实的角度考虑,虽然不能实现理想的分布式系统,但我们是否可以通过对系统主要设计指标进行一定的妥协,来设计出一个理论上可行的、可以满足实际需求的分布式系统呢?
Trade-off
幸运的是,由Eric Brewer等人提出的 CAP定理 已经为我们回答了这个问题。 CAP定理 的一个表述是:
CAP定理分布式计算系统不可能同时确保一致性、可用性和分区容忍性。
一致性(Consistency) :所有节点在同一时刻能够看到同样的数据,也即“强一致性”;
可用性(Availability) :确保每个请求都可以收到确定其是否成功的响应;
分区容忍性(Partition tolerance) :因为网络故障导致的系统分区不影响系统正常运行。
这也就意味着,我们虽然不能使某个分布式场景同时满足三个性质,但可以使之同时满足三个中的两个。更进一步说,对于包含多个分布式场景的分布式系统,我们甚至可以在三个性质的程度上进行适当的权衡。
CAP权衡方案
我们把解决一致性问题(Consensus Problem)的算法叫做一致性算法(Consensus Algorithm)或者一致性协议(Consensus Protocol)。CAP定理能够将这些一致性算法的集合进行归类:
C+A :以2阶段提交(2 phase commit)为代表的严格选举协议。当通信中断时算法不具有终止性(即不具备分区容忍性);
C+P :以Paxos、Raft为代表的多数派选举算法。当不可用的执行过程超过半数时,算法无法得到正确结果(即会出现不可用的情况);
A+P :以Gossip协议为代表的冲突解决协议。当网络分区存在和执行过程正确时,只能等待分区消失才保持一致性(即不具备强一致性)
基于CAP定理,我们需要根据不同场景的不同业务要求来进行算法上的权衡。对于分布式存储系统来说,网络连接故障是无法避免的。在设计系统时不得不考虑分区容忍性,所以我们实际上只能在一致性和可用性之间进行权衡。
强一致性与可用性的矛盾会导致十分令人头疼的抉择。在实际情况中,对于不是那么重要的数据的存取操作,往往会调低一致性来增加可用性。如GeneDock的账户信息管理数据,是以最终一致性的方案分发到各个业务域的,这样既满足了各域业务API的性能需求,又使得跨域的账户信息同步功能得以实现。当然,对于敏感的元数据信息,GeneDock采取的则是强一致性的方案。
知名分布式系统的主场景设计权衡
特别值得一提的经典设计范例是阿里巴巴的OceanBase系统。它将数据分为了冷数据和热数据两个不同的场景。对于冷数据,规定只读不写。这样就不需要处理分布式写操作带来的一致性问题,只需保证可用性和分区容忍性即可(即AP场景)。而对于新增的热数据,由于用户需要频繁访问,所以采取不同的服务器分片进行服务,本地读写的模式,不需要考虑网络分区的问题(即CA场景)。通过对CAP定理的深刻理解和灵活运用,构建出了满足高并发读写、处理海量金融数据的分布式数据库。
Summary
在计算的世界里,一切都是有代价的。 我们必须根据业务实际场景,在关键的业务指标中进行权衡,进而决定合适的解决方案。必须承认,很多系统声称能够解决的问题其实已经被理论证明是不可实现的,这也客观上要求用户在选择云服务提供商的时候一定要擦亮眼睛,不能被过度的宣传所误导。
GeneDock的分布式系统解决方案是在深入考量了生物信息分析领域的实际需求,对许多问题做了艰难权衡之后才确定下来的,已经经受住了近两年的大规模商业计算和存储业务的考验。无论是在针对计算量巨大的全基因组分析或BLAST等分析任务,还是在大规模基因数据的存取及传输场景中,GeneDock对解决方案都进行了精心的设计和实现,确保任务运行的稳定性、数据存储的可靠性和数据传输的正确性,同时使整体系统运行结果准确一致。
参考资料一致性问题:https://en.wikipedia.org/wiki/Consensus_(computer_science)FLP不可能性:http://cs-www.cs.yale.edu/homes/arvind/cs425/doc/fischer.pdfCAP定理:https://en.wikipedia.org/wiki/CAP_theorem