免费注册 查看新帖 |

Chinaunix

  平台 论坛 博客 文库
最近访问板块 发新帖
查看: 1226 | 回复: 0
打印 上一主题 下一主题

分布式系统/协议的一种形式化分析方法——Knowledge [复制链接]

论坛徽章:
0
跳转到指定楼层
1 [收藏(0)] [报告]
发表于 2011-12-19 13:54 |只看该作者 |倒序浏览
<p>前两天看到一篇应该属于“计算机科学”而非“计算机技术”的文章,“Knowledge and Common Knowledge in a Distributed Environment”,很遗憾,根据我目前有限的知识和更为有限的精力,并不能完全读懂这篇文章,只是能了解个大概意思。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 在作者(Halpern,Moses)看来,一个分布式系统中的各个节点所拥有的Knowledge状态,在这个分布式系统中扮演着极其基础的角色。对这种Knowledge状态的描述和理解,可以用于设计一个分布式协议,证明该协议的属性,理解一个分布式系统的运行等。文章中使用了形式化的方法来定义系统、Knowledge极其状态,并且使用这些定义证明了两个经典的问题。作者认为,该形式系统可以用于解决(当然指的是理论上的证明)一般性的分布式系统问题。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 注:原文大量使用了形式化的定义,在数学上十分严谨,而本文不再使用那些定义,只是给出我对它们的理解。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 什么是一个分布式系统?直观上讲,一个分布式系统包含一组相对独立的计算节点{p1, p2, p3, … , pn};每个节点的行为仅仅由它本地的信息决定;节点通过某种网络进行连接,节点之间只能通过消息传递进行通信。这里面,“节点本地的信息”和节点的knowledge关系十分紧密。假设存储足够,每一个节点的本地信息包括该节点初始时知道的信息,它接收到的所有消息和它观察到的所有事件。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 一个节点的Knowledge就是由该节点的本地信息可以知道的所有的事实。当然,Knowledge不单单可以关联在一个节点上,我们也可以讨论一组节点所拥有的knowledge。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 先看一个例子:一个家庭有好些个孩子,比如n个,这些孩子每天都一起出去玩,一起回来。如果一个孩子的额头上沾了泥巴,妈妈就会惩罚他。每个孩子可以看到别的孩子额头上是否有泥巴,却看不到自己的。同时,每个孩子都乐于看到别人受到惩罚,所以不会主动告诉别人额头上是否有泥巴。有一天,这些孩子同时回到家门口,恰好爸爸回来了,爸爸告诉他们说,“至少有一个人的额头上有泥巴”。之后,爸爸开始不断地重复一个问题,“谁头上有泥巴请回答yes,没有的请回答no”。假设每个孩子在不确定自己是否有泥巴时,都会认为自己没有,会回答“no”,只有确定自己有泥巴时,才会回答“yes”。所有的孩子每次都是同时回答的,他们都是诚实且有足够的逻辑能力的。问题是如果有k个孩子头上有泥巴,会出现什么现象?</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 答案:在爸爸的前k-1个问题时,所有人都回答no,第k个问题时,有泥巴的所有小孩回答yes,其他回答no。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 对于这个问题,网上有很多变种,也有详细的解释,此处不再赘述。问题在于,如果k&gt;=2,那么每个小孩其实自己都知道“至少有一个人的额头上有泥巴”这个事实,如果爸爸不宣布这句话而直接开始提问,那么无论问多少次,所有的孩子都会回答no。但是,爸爸宣布了一件本来大家都知道的事情之后,再开始提问,情况却发生了改变,为什么?直观上推测,爸爸宣布“至少有一个人的额头上有泥巴”,一定还包含了另外的信息,这些信息使得每个小孩的knowledge的状态发生了变化。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 在本文中,作者将一个分布式系统的knowledge分成了几类,这几类根据它们之间的包含关系,构成了一个层次。如下所述:</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 假设f是一个事实,如果节点i的知道f,我们就说节点i拥有关于f的knowledge,记做K[i](f) |= true,或者f 属于集合K[i]。我们把一个分布式系统中的节点的集合记做G。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; D[G](f) |= true:系统G拥有关于f的Distributed Knowledge。如果存在一个系统G之外的实体,该实体知道G中每个节点的Knowledge,那么该实体知道f,此时,我们称G拥有关于f的Distributed Knowledge。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; S[G](f) |= true:G中某个节点知道f。即S[G](f)等于K[i](f)的或。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; E[G](f) |= true:G中每个节点都知道f。即E[G](f)等于K[i](f)的与。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; E^k[G](f) |= true:G中每个节点都知道E^(k-1)[G](f) |= true。这个需要解释下,假如说f是“昨天吃排骨了”,E[G](f) |= true表示G中每个节点都知道“昨天吃排骨了”,而E^2[G](f) |= true表示G中每个节点都知道 每个节点都知道“昨天吃排骨了”,依此类推。呵呵,类似与“我知道 你知道我知道”。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; C[G](f) |= true:当且仅当E[G](f) |= true 且 E^2[G](f) |= true且…且E^k[G](f) |= true 且…。这被称为系统G的Common Knowledge。理论上讲,Common Knowledge是一个系统G各个节点之间最强的一种agreement(唉,没想好应该选哪个中文词来表达这个意思,大概是“关于xxx的意见高度统一”吧)。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 有了这种knowledge的分层定义,我们再来看前面提到的那个问题。我们仅仅看k==2的情况,其它情况可以用数学归纳法证明。此时,我们假设所有小孩构成的分布式系统是G,额头有泥巴的小孩分别是a和b,f代表“至少有一个人的额头上有泥巴”这个事实。在爸爸宣布f之前,有E[G](f) |= true,即每个孩子都知道f,但是,E^2[G](f) |= false,即,并不是每个人都知道每个人都知道f。比如,a就不知道b知道f,而第三个小孩c知道a不知道b知道f。而爸爸宣布f,使得E^2[G](f) |= true,即每个人都知道每个人都知道f,由于多了这些信息,或者说系统G关于f的knowledge的状态变得更强了,导致了孩子可以在爸爸第二次问问题的时候判断出自己的额头上是否有泥巴。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 对于一般的k,如果Ek[G](f) |= true,那么孩子们在父亲第k次提问的时候就会判断出自己的头上是否有泥巴,否则,无法判断。而父亲宣布f这件事,其实使得C[G](f) |= true。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 再来看一个问题:有一个山谷,两边的山上驻扎着红军,谷中驻扎的蓝军。如果山谷两侧的红军同时攻击,就会取胜,而如果一侧攻击,而另一侧没有同时攻击,就会让蓝军突围。两侧红军的将军只有确认对方会和自己一起攻击的情况下才会发起攻击。两侧红军只能通过通讯员传递消息,通讯员可能在路上被蓝军杀死。问题是,是否可以设计一种协议,使得红军的两个将军可以达成一致并发起攻击?</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 答案:不可能设计出这样的协议。具体解释也请参考网上众多的文章。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 现在我们来看为什么。假设一个理想情况,在红军相互传递消息的时候,运气非常好,没有一个通讯员被蓝军杀死。设两侧红军分别是a和b,a想“在明天12点发起进攻”,所以首先向b派出通讯员。我们用f表示“在明天12点发起攻击”这个“事实”。当第一个通讯员到达b时,E[G](f) |= true,但是E^2[G](f) |= false;a和b通过不断地向对方派出通讯员并接收对方的通讯员,对于任意一个有限k,可以做到E^k[G](f) |= true,但是,在有限的步骤中却达不到C[G](f) |= true。而事实上,对于任何一个有限的k,E^k[G](f) |= true都不能使得a和b进行攻击,只有C[G](f) |= true时,两边才会进行攻击。证明的方式仍然是数学归纳法。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 在文章中,作者证明了一个定理:在一个分布式系统G中(节点数&gt;=2),如果通信不是可靠的,那么,不可能通过通信来达到对于某个事实f的C[G](f) |= true。换句话说,在这样一个系统中,对于任何一个事实f而言,要么不需要任何通信,已经是C[G](f) |= true了(例如,每个节点都知道每个节点的配置文件中都有一个“明天12点攻击”);否则,无论怎么通信,f也不可能变成C[G](f) |= true。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 看到这个结论的时候,让我又受了一次打击。这岂不是说,在任何实际使用的分布式系统中,都无法通过通信的方式,使得C[G](f)由false变为true吗?现在的分布式系统中的节点是怎么通过协商确定配合完成某件事的?</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 题外话:什么时候总结下计算机科学家们让我受的各种打击,呵呵。一下子能想到的只有两个:</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 本科时《可计算性理论》课上第一次明确知道世界上存在(还存在非常非常多)计算机不可判定的问题——“停机问题不可判定”的证明。这之前我一直认为计算机可以解决所有人脑可以解决的问题(包括制造与人一样的机器人),只是我们还没想出来好的算法或者计算机的性能还不够。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 研究生做编译即编译优化时在程序分析课上知道了rice那哥们证明了“关于程序的任何非平凡属性都是不可判定的”这个定理,而平凡属性只剩下“所有程序都真,或者对所有程序都假的属性”。看完证明后的第一个想法是“这还怎么做编译优化?!”。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 想想我们常见的那些分布式算法/协议,它们主要的困难点就在于协调系统中各个节点的行为,使得各个节点在某些方面达成一致。用作者的话说,这些协议做的很重要的两件事就是“发现某个事实f”和“发布f,使的C[G](f) |= true”,只有系统中的各个节点拥有Common Knowledge,才能协调工作啊。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp; 还好,实践中的分布式系统并不是一定需要严格的Common Knowledge才能工作,就好象即使rice证明了rice定理,gcc仍然有上百中优化一样。实践中使用的Common-Knowledge并不是理论上那么严格的,而是一些弱化的变体。在该文章中,作者举了两个例子,分别是e-Common Knowledge(‘e’代表epsilon)和eventually-Common Knowledge。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 这篇文章提出的这个形式化的方法,可以用于从理论上证明分布式系统/协议的“可能”与“不可能”,同时,对这种想法有个了解后,对于我们自己去理解别的分布式系统,也有一定的帮助。</p>  <p>&nbsp;</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 看了这篇文章,还想再唠叨几句。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 我从小就很fan“科学”,现在一点也没变。大学本科学计算机时,有一段时间非常郁闷,那时学到的都是些工程技术,完全不像数学、物理那样。那时,我觉得跟别人说“我会计算机”和说“我会修自行车”一样,这是一种纯技术的活动。而我fan的人却是那些提出并证明“自行车的轮子应该是圆的”或“自行车可以保持平衡”的人。这种郁闷直到看了《自动机理论基础》和《可计算性导引》之后。再之后,终于逐渐的感觉到了离散数学和计算机程序的联系。也看了一些纯理论的文章。我才相信,计算机是包含“科学”部分的。</p>  <p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 比较遗憾的是,今天我从事的几乎所有的工作,都只是工程技术。书店里计算机相关的书籍中,绝大部分都是在讲各种各样的技术;这大概是计算机界的规则吧。</p>
您需要登录后才可以回帖 登录 | 注册

本版积分规则 发表回复

  

北京盛拓优讯信息技术有限公司. 版权所有 京ICP备16024965号-6 北京市公安局海淀分局网监中心备案编号:11010802020122 niuxiaotong@pcpop.com 17352615567
未成年举报专区
中国互联网协会会员  联系我们:huangweiwei@itpub.net
感谢所有关心和支持过ChinaUnix的朋友们 转载本站内容请注明原作者名及出处

清除 Cookies - ChinaUnix - Archiver - WAP - TOP