Improvement Of Raft Consensus Algorithm And Proof Of Correctness In SDN Multiple Controllers

With the expansion of the software-defined network scale and the complication of upper-layer applications,a single controller cannot meet network requirements and becomes a bottleneck in network performance.There are many advantages of managing SDN through the multi-controller cluster,but the most basic problem that needs to be solved in implementing the multi-controller architecture is the consistency among multiple controllers.The consistency problem can be solved by running the Raft consensus algorithm in the cluster,but the re-election of the leader will cause the cluster to be unavailable.Therefore,considering the availability of the cluster,the leadership transfer function is added to the Raft algorithm to prevent the cluster from being unavailable because of the leader being shut down or the leader being removed from the cluster and so on.The main research contents of the thesis are as follows:Firstly,the situations that the leadership can be transferred in the leader election of the Raft algorithm are classified in detail,and the metrics and the methods for selecting target nodes are given.For the operating characteristics of multi-controller clusters,the appropriate indicators are selected to obtain the target controller.Secondly,the TLA+ language is used to formally specify the leadership transfer function,and the TLC Model Checker is used to check and verify the Raft algorithm specification with the leadership transfer to prove its correctness.Thirdly,the operating environment of the Raft algorithm in a multi-controller cluster is discussed,specified using the TLA+ language,and checked and verified using the TLC Model Checker.At last,the codes of the leadership transfer in the Raft algorithm implemented by OpenDaylight cluster are analyzed,and the election time and the time of leadership transfer when the leader is required to shut down of the OpenDaylight cluster are measured.In summary,the situations that the leadership can be transferred in the leader election of the Raft algorithm in multiple controllers are classified in detail,and metrics and methods for selecting target nodes are presented.A precise formal specification of the Raft algorithm with leadership transfer is specified with the TLA+ language,and its correctness is checked and verified with the TLC Model Checker.The conclusion that the leadership transfer function improves the availability of the cluster is obtained by comparing the timeout election time and the time of leadership transfer when the leader is asked to shut down of the OpenDaylight cluster.