Vanlightly commented on pull request #1690: URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-916196689
I have finished my review of the spec against the code and I do not find any problems in terms of correctness. There are however, a number of suggestions. - Some action names are not very helpful, see my comments in code - The FastLeaderElection module is too focused on the production implementation in my opinion. One of the benefits of TLA+ is being free of programming considerations like multi-threading. The fact that the FastLeaderElection implementation uses the internal queues recvqueue and sendqueue is an implementation detail that we don't need to replicate in the TLA+. I think you could combine ReceiveNotmsg with HandleNotmsg. Also the WaitNewNotmsg and WaitNewNotmsgEnd are not optimized for state space and are also perhaps, implementation oriented. I think there are some big opportunities to make FLE simpler and with a smaller state space. - Consider adding the test variables of ZabWithFLETest to the main spec, using a view to remove those variables from state space exploration and using state constraints to limit state space exploration using those variables. Then this test spec is not required. - Add some additional comments to explain what is going on in each action. The above are not blockers, just suggestions. -- 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: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
