You are viewing a plain text version of this content. The canonical link for it is here.

Posted to notifications@zookeeper.apache.org by GitBox <gi...@apache.org> on 2021/07/15 08:01:08 UTC

[GitHub] [zookeeper] BinyuHuang-nju commented on pull request #1690: ZOOKEEPER-3615: Provide formal specification and verification using TLA+ for Zab

BinyuHuang-nju commented on pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-880483752


   @hanm @Vanlightly Hi! Now I have pushed spec of zab-1.0 here.
   In spec, I use action RECOVERYSYNC to abstract the phase of SYNC before leader sending NEWLEADER.
   Due to the differences between formal specification and engineering implementation, and the purposes of reducing state space, there are differences in my expression and code in some places. But I think this does not affect the equivalence between the two.
   For example, in spec, only the leader in broadcast phase will accept the requests, which is to omit the extra space brought by the follower’s acceptance of client’s request.
   I will be very glad to see your feedbacks! And I will reply to you as soon as possible if you have any question!


-- 
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.

To unsubscribe, e-mail: notifications-unsubscribe@zookeeper.apache.org

For queries about this service, please contact Infrastructure at:
users@infra.apache.org