hanm commented on a change in pull request #1690: URL: https://github.com/apache/zookeeper/pull/1690#discussion_r630726805
########## File path: zookeeper-contrib/zookeeper-contrib-zabtla/experiment/ZabWithQTest.tla ########## @@ -0,0 +1,994 @@ +(* + * Licensed to the Apache Software Foundation (ASF) under one + * or more contributor license agreements. See the NOTICE file + * distributed with this work for additional information + * regarding copyright ownership. The ASF licenses this file + * to you under the Apache License, Version 2.0 (the + * "License"); you may not use this file except in compliance + * with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + *) +-------------------------------- MODULE ZabWithQTest -------------------------------- +\* This is the test for formal specification for the Zab consensus algorithm, Review comment: Can we make this module extends Zab module to avoid copy / paste? ########## File path: zookeeper-contrib/zookeeper-contrib-zabtla/README.md ########## @@ -0,0 +1,71 @@ +# Zab-tla + +## Overview +This project is devoted to providing formal specification and verification using TLA+ for the Zookeeper Atomic Broadcast(Zab) consensus protocol proposed in *Junqueira F P, Reed B C, Serafini M. Zab: High-performance broadcast for primary-backup systems[C]//2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, 2011: 245-256*. Review comment: Sounds like this PR is specifically scoped to the paper (which is kind of out of date), which is totally fine. Just want to point out that the actual ZAB running in ZooKeeper production today is ZAB 1.0 while the algorithm described in the paper is pre-1.0 and there are a few changes between the two. There is a canonical description of ZAB 1.0 here: https://cwiki.apache.org/confluence/display/ZOOKEEPER/Zab1.0. It would be more practically impactful if we have a specification checking the modern version of protocol but that can certainly be done after this exercise. ########## File path: zookeeper-contrib/zookeeper-contrib-zabtla/README.md ########## @@ -0,0 +1,71 @@ +# Zab-tla + +## Overview +This project is devoted to providing formal specification and verification using TLA+ for the Zookeeper Atomic Broadcast(Zab) consensus protocol proposed in *Junqueira F P, Reed B C, Serafini M. Zab: High-performance broadcast for primary-backup systems[C]//2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, 2011: 245-256*. + +We have made a formal [specification](Zab.tla) for Zab using TLA+ toolbox, and we have done a certain scale of model checking to verify the correctness of Zab. + +Due to the simplification of Zab algorithm description in the paper, some details in specification were modified and added. If you have any question, please let us know. + +You can find this document in chinese in [doc-in-chinsese](doc-in-chinese/README.md). + +## Requirements +TLA+ toolbox version 1.7.0 + +## Run +Create specification and run models in the usual way. Review comment: I would recommend we put more descriptions on the steps to run the TLC model checker on this specification. In particular, the configurations like invariants, constraints, etc, so everyone who is interested can trivially reproduce (I see the previous discussions in this PR largely related to figure out this). What some other projects do is to also commit the toolbox configuration files (the .toolbox folder), maybe we can also consider doing the same. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. For queries about this service, please contact Infrastructure at: [email protected]
