SDN多控制器环境下对Raft一致性算法的改进及正确性证明

摘要

随着软件定义网络（software-defined network，简称SDN）规模的扩大和上层应用的复杂化，单个控制器已经不能满足网络要求，成为网络性能的瓶颈。多控制器集群管理SDN有很多优势，但实现多控制器架构需要解决的最基本问题是多控制器之间保持一致性。在集群中运行Raft一致性算法可以解决一致性问题，但集群中Leader被重新选举时会导致集群不可用。因此本文从集群的可用性出发，为Raft算法增加领导权转移功能，避免因Leader被要求关闭、移出集群等情形导致的集群不可用。本文主要研究内容有：
　　第一，对Raft算法选举部分可以转移领导权的情形进行详细分类，给出选择目标节点的度量与方法。针对多控制器集群的工作特点，选取合适的指标选择目标控制器。
　　第二，使用TLA+语言对领导权转移功能进行形式化描述，并使用TLC工具对增加领导权转移的Raft算法的形式化描述进行检测与验证，从而证明其正确性。
　　第三，讨论多控制器集群中Raft算法的运行环境，使用TLA+语言描述并使用TLC工具对规约进行检测与验证。
　　第四，分析了OpenDaylight（ODL）代码中的Raft算法源码的领导权转移部分，并对选举用时与Leader被要求关闭时发生领导权转移的用时进行了测量。
　　综上所述，本文对Raft算法选举部分中可以发生领导权转移的情形进行详细分类，给出选择目标控制器的具体指标与方法。使用TLC工具检测与验证加入领导权转移的Raft算法的TLA+规约的正确性。并通过测试ODL集群正常超时选举用时与Leader被要求关闭时发生领导权转移的用时验证了当Leader被要求关闭时领导权转移功能可以提高集群的可用性的结论。

目录

第一个书签之前