Specification and Verification of the Zab Protocol with TLA+
- PDF / 499,622 Bytes
- 12 Pages / 595 x 842 pts (A4) Page_size
- 87 Downloads / 269 Views
Specification and Verification of the Zab Protocol with TLA+ Jia-Qi Yin1 , Hui-Biao Zhu1,∗ , M ember, CCF , and Yuan Fei2,∗ , M ember, CCF 1 2
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China College of Information, Mechanical and Electrical Engineering, Shanghai Normal University, Shanghai 200234, China
E-mail: [email protected]; [email protected]; [email protected] Received April 11, 2020; revised October 9, 2020. Abstract ZooKeeper Atomic Broadcast (Zab) is an atomic broadcast protocol specially designed for ZooKeeper, which supports additional crash recovery. This protocol actually has been widely adopted by famous Internet companies, but there are few studies on the correctness and credibility of the Zab protocol, and thus we utilize formal methods to study the correctness. In this paper, Zab, Paxos and Raft are all analyzed and compared to help better understand the Zab protocol. Then we model the Zab protocol with TLA+ and verify three properties abstracted from the specification by the model checker TLC, including two liveness properties and one safety property. The final experimental results can prove that the design of the protocol conforms to the original requirements. This paper makes up for the analysis of formal methods in the Zab protocol. Keywords
1
Zab protocol, TLA+, specification, verification
Introduction
With the emergence of distributed architecture, more and more distributed applications will face the problem of data consistency. It is a little pity that, as far as we know from our investigation, there is no mature and stable solution that has been applied on 1 large-scale systems except ZooKeeper○ , which is modeled after Google’s Chubby [1] . The core protocol of ZooKeeper is the Zab (Zookeeper Atomic Broadcast) protocol [2] . As the most mature, stable and recognized solution, Zab does not analyze the correctness of the whole design from the perspective of the first-order logic and set theory, and it does not help relevant programmers or practitioners understand the algorithm more intuitively. Raft, similar to Zab, has been studied a lot to help us understand its complexity, but there are few studies on Zab. Therefore, we first give the similarities and differences among Raft, Paxos and Zab to
help us grasp these sophisticated protocols. Then, we employ TLA+ proposed by Lamport [3] to assist in understanding the Zab protocol from the perspective of first-order logic, and verify the properties that should be satisfied in Zab’s design through its corresponding model checker TLC. In our specification modeling and verification, the first thing to consider is the five basic attributes [2] that Zab must satisfy. Single Leader per Epoch. Only one leader is allowed to exist in each cycle, and it has the largest epoch in its cycle. A leader must be approved by more than half of the followers. Highest Transaction Identifier. Since there is only one largest epoch in each cycle, the transaction to be processed can only have the highest z
Data Loading...
