search

zk1931 / jzab

ZooKeeper Atomic Broadcast in Java
http://zk1931.github.io/jzab/master/
Apache License 2.0
54 stars 23 forks source link

Use TLA+ to specify javazab #92

Open ghost opened 10 years ago

ghost commented 10 years ago

We try to follow the zab paper carefully, but we might make wrong assumptions that impact the correctness of our implementation. It would be nice to have a TLA+ specification for javazab.

http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html https://ramcloud.stanford.edu/~ongaro/raft.tla

fpj commented 10 years ago

That's an interesting request. I think your high level goal is to be able to check if this implementation is correct with respect to the protocol description. Assuming you get a spec, are you planning on checking with the model checker? Are you after a spec of zab so that you can use for a refine mapping? Just writing a spec might help to catch some bugs, but it isn't going to tell you for sure whether it is right or wrong.

ghost commented 10 years ago

I was originally thinking to specify our implementation and check it against the model checker. It would also be interesting to have a spec for zab itself.