Formalization And Verification Of Redis Cluster Message Communication Mechanism Based On CSP

With the advent of the era of big data,traditional databases have been difficult to meet data access under high concurrency.Redis in-memory databases are widely used because they can provide high performance and stability for big data.Redis not only supports multiple types of data structures,transaction functions,subscription and release mechanisms,but also features such as automatic fault handling.With the increase in the amount of data in the application,Redis Cluster solves the problems of heavy server load and memory bottleneck under a single machine.However,as the Redis Cluster solution is widely used,problems such as inefficient data synchronization and load balancing optimization after failover also occur.To ensure high performance and high availability of the Redis Cluster,it is necessary to conduct modeling analysis and research on the Redis Cluster from a formal perspective.The research object of this paper is the Redis Cluster message communication mechanism,its purpose is to achieve the consistency and availability of the cluster.Based on the high-confidence characteristics of the formal method and the requirements of Redis Cluster consistency and availability,Communicating Sequential Processes(CSP)is used to formally analyze and verify the Redis Cluster message communication mechanism.By analyzing the behavior of each entity of message communication,the whole system is abstracted into two modules of Meet message communication and Ping-Pong message communication,and the definitions of related collections,messages and channels are given.CSP model of Redis Cluster message communication mechanism is constructed.Next,the model detection tool PAT(Process Analysis Toolkit)is used to perform code implementation on the constructed CSP model.The definition of constants,variables,channels and code implementation of Meet message communication and Ping-Pong message communication process are completed.Then,the definition and implement of properties of the model to be verified are given.It can be seen from the results that the Meet message communication module satisfies deadlock free and exchangeability,that is,the two nodes shaking hands can exchange messages.In addition,the Ping-Pong message communication module satisfies deadlock free,endability,propagability,and final consistency,that is,the message of any node can always be obtained by other nodes in the cluster.This paper proves that the Redis Cluster message communication mechanism can guarantee the consistency of the cluster through a rigorous formal verification method.Finally,based on the Redis Cluster message communication mechanism,the Redis Cluster fault handling mechanism was introduced.The three processes of replication,fault detection,and failover were analyzed and the CSP model of the Redis Cluster fault handling mechanism was constructed.Then the command propagation of the model fault testability and fault transferability are verified.,thus ensuring high availability of Redis Clusters.Subsequently,in view of the inefficiency of data synchronization after failover,by introducing the parent node chain,an optimized solution that converts the complete synchronization of network bandwidth and computing resources into partial synchronization with high efficiency and low energy consumption was proposed,and passed Formal methods verify the effectiveness of the scheme.