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

[GitBox <gi...@apache.org>]

Vanlightly commented on pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-974609840


   @BinyuHuang-nju I have checked it over and it's looking good. There's just one last point from my perspective.
   
   The Value constant is not really that useful as it stands right now. It is still possible for a client to write the same value more than once. More importantly the values are not checked in any invariants, so the values do not serve any purpose right now other than to increase the state space. 
   
   I would recommend adding a value equality check to `TransactionEqual` to ensure that not only the zxid matches but the value also. Then also prevent the same value from being written twice in `ClientRequestAndLeaderBroadcastProposal` and remove the check for transaction num.
   


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