Hi Andor, I am writing to inquire about the possibility to include the TLA+ specifications for ZooKeeper in the upcoming release, version 3.9.0. The proposal to provide TLA+ specifications for ZooKeeper was raised in ZOOKEEPER-3615<https://issues.apache.org/jira/browse/ZOOKEEPER-3615>, and addressed via pull request #1690<https://github.com/apache/zookeeper/pull/1690> on github.
Formal specifications can serve as precise documentation of the Zab design and implementation, and can help eliminate any ambiguities in the informal protocol description, which would be beneficial for ZooKeeper learners and developers. Popular consensus protocols like Paxos and Raft also provide their TLA+ specifications. It would be great to merge the pull request and include the TLA+ specifications for ZooKeeper in the new version. I have also raised a request for the review of pull request #1690<https://github.com/apache/zookeeper/pull/1690> to the ZooKeeper developer mailing list. More details can be found at https://lists.apache.org/thread/ww4v1r733whcds64jg5wt7ozclbjhdr0 . Looking forward to your feedback! Best regards, Sirius 2023年6月15日 19:57，Andor Molnar <an...@apache.org<mailto:an...@apache.org>> 写道： Hi folks, There're 64 open tickets which has fixVersion = 3.9.0 I'll remove the fixVersion from all of them except the ones that we marked as release blockers. Currently: - ZOOKEEPER-4393 Problem to connect to zookeeper in FIPS mode - ZOOKEEPER-4622 Add Netty-TcNative OpenSSL Support - ZOOKEEPER-4655 Communicate the Zxid that triggered a WatchEvent to fire Please let me know if you would like to add anything to this list. Regards, Andor
