4.1.3 降低通信复杂度
在多数情况下,有一个简单的优化[1]可以用来减少通信复杂度,虽然它不能降低最坏情况下复杂度的数量级。也就是说,进程可以只在它们初次知道max-uid的时候发送消息,而不是在每轮中都要发送。我们把这个算法叫作优化洪泛最大值算法(OptFloodMax)。对洪泛最大值算法的代码修改如下:
优化洪泛最大值算法:
很容易相信这个改进算法是正确的,然而怎样形式化地证明它呢?一个方法就是使用在洪泛最大值算法中用过的不变式断言。但这涉及对许多已做工作的重复。我们不从头开始,而是给出一个证明,基于优化洪泛最大值算法和洪泛最大值算法在形式化上的相关性。这个简单例子表明,可以使用模拟的方法来证明分布式算法的正确性。
定理4.2 在优化洪泛最大值算法中,在diam轮内,进程imax输出自己为领导者,其他的进程输出自己为非领导者。
证明 和断言4.1.1相似,我们可以很容易地证明以下断言。
断言4.1.5 在diam轮后,对于每一个j≠imax,和statusj=non-leader。
我们现在先证明一个预备的不变式,它表明只要进程预期在下一轮中需要发送新信息,进程的new-info标志就设置为true。特别地,如果i的任一出向邻接节点不知道这样一个UID,该UID不小于i已知的最大UID,那么i的new-info标志就必定为true。
断言4.1.6 对任意的r(0≤r≤diam)和任意的i,j,其中j∈out-nbrsi,在r轮之后,如果max-uidj<max-uidi,则new-infoi=true。
断言4.1.6可以通过对r的归纳来证明。基本情况是r=0为真,因为所有的new-info标志都被初始化为真。下一步,我们考虑进程i和j,j∈out-nbrsi。如果max-uidi在r轮中变大,那么new-infoi就设置为真,满足结论。另一个方面,如果max-uidi没有增大,那么归纳假设表明,要么max-uidj已经足够大,要么new-infoi刚好在r轮前为真。在前一种情况下,max-uidj保持足够大,因为这个值从来不减小。在后一种情况下,新的信息在第r轮会被从i发送到j,导致max-uidj变得足够大。
现在,来证明优化洪泛最大值算法的正确性,我们假想优化洪泛最大值算法和洪泛最大值算法一起运行,以同样的UID赋值开始。证明的核心部分是模拟关系,它涉及相同轮数之后两种算法所处状态的不变式断言
断言4.1.7 对于任意的r,0≤r≤diam,在r轮后,u、max-uid、status和rounds分量的值在两种算法中都是一样的。
断言4.1.7的证明通过对r的归纳进行,就像只包括单个算法的常见的断言一样。在归纳步骤中重要的部分就是表明max-uid的值保持相同。
所以考虑任意的i和j,其中j∈out-nbrsi。如果在第r轮前new-infoi=true,那么就和在洪泛最大值算法中一样,优化洪泛最大值算法的进程i也在第r轮向j发送相同的信息。另一方面,如果在第r轮前new-infoi=false,那么在优化洪泛最大值算法中,i不向j发送任何东西,但是在洪泛最大值算法中,i向j发送max-uidi。断言4.1.6表明,在r轮前,如果max-uidj≥max-uidi,那么在洪泛最大值算法中,消息对max-uidi是无影响的。在两个算法中,i对max-uidi有相同的影响。既然这个对所有的i和j来说都是真的,那么在两个算法中,max-uid的值就会保持相同。
断言4.1.7和断言4.1.1共同证明了断言4.1.5。
刚才我们证明优化洪泛最大值算法正确性的方法在证明“优化的”分布式算法的正确性时很有用。首先,证明一个低效率但是简单的算法的正确性。然后,通过证明两个算法之间的一个形式化关系,来证明更有效但是更复杂的算法的正确性。对于同步的网络算法来说,这种关系一般采取上面的形式——包括相同轮数之后两个算法的状态的一个不变式。
另一个改进 我们可以在洪泛最大值算法中稍微减少消息个数。也就是说,如果进程i接收到来自进程j的一个新的最大值,其中j既是i的出向邻接节点也是i的入向邻接节点,即i与j有双向通信,那么i在下一轮的时候就不需要向j的方向发送消息。
在一个具有UID的一般有向图网络中,进程不知道节点数n和直径diam,也是可能选出领导者的。现在我们建议你停下来去构造一个这样的算法。一种可能的方法是引入一种辅助协议来允许每个进程计算网络的直径。本章中稍后讲到的思想或许有用。