3 ms·
Do they publish formal specifications of these distributed algorithms? Has anyone verified the implementation? Zookeeper is at least based on Paxos which has
by agentultra 10y ago
Do they publish formal specifications of these distributed algorithms?
Has anyone verified the implementation?
Zookeeper is at least based on Paxos which has a TLA+ model one can check.
- emirozer 10y agoIt's based on Raft : https://github.com/coreos/etcd/tree/master/raft https://github.com/coreos/etcd/tree/master/raft https://raft.github.io/ https://raft.github.io/
- philips 10y agoWe also do a ton of functional testing as code is merged to test lots of different partitions and faults. You can read more on this post: https://coreos.com/blog/new-functional-testing-in-etcd/ https://coreos.com/blog/new-functional-testing-in-etcd/
- ideal0227 10y agoetcd is based on Raft. Raft has a TLA+ spec. But do note that the implementation usually diverges from its algorithm [0]. For etcd, we try to keep the core algorithm as self-contained and deterministic (no I/O, no timer) as possible. So it can be very close to the pure algorithm. We are very confident about it since we throughly tested it, and the implementation is shared with other consistent large scale database systems too (cockroachdb, tikv). ZooKeeper uses ZAB [1] under the hood. I do not think there is a TLA+ for ZAB. [0] https://www.cs.utexas.edu/users/lorenzo/corsi/cs380d/papers/paper2-1.pdf https://www.cs.utexas.edu/users/lorenzo/corsi/cs380d/papers/... [1] http://www-users.cselabs.umn.edu/classes/Spring-2016/csci8211/Papers/Distributed%20Systems%20Zab-%20High-performance%20broadcast%20for%20primary-backup%20systems.pdf http://www-users.cselabs.umn.edu/classes/Spring-2016/csci821...
- agentultra 10y agoRaft - cool! I'm aware that implementations diverge or do not directly synthesize from their specifications. At least not yet. I'll be poking around more to see if the etcd team has published their own specs for the novel parts of the system. I'm particularly interested in seeing if/how OSS projects are adopting more rigorous "engineering" practices.
- carterschonwald 10y agoI took a look at the etcdv3 raft.go code, it is indeed pretty nicely written! Definitely better than any other one i've seen. (though i'm pretty excited about the raft impl my summer intern and I are hacking on currently :) )
- cstrahan 10y agoIn Haskell, I presume? Will it be open sourced? :)
- carterschonwald 10y agoActually doing in Agda first. Coinductive programming is a delight with Agda 2.5. But yes that's the plan.
- sagichmal 10y agoConsul's Raft implementation is leagues better than etcd's, unfortunately.
- eis 10y agoIs that still the case with Etcd v3? I remember reading somewhere that they were rewriting the Raft implementation in Etcd a good while ago.
- justinsb 10y agoI'd be very interesting in hearing more about this. I tried using both the Consul and etcd Raft implementations as libraries. I found the Consul library much easier to interface with. But it was my impression that the etcd library was much more tested in the real-world, with big projects like Kubernetes and with the library being embedded into projects like CockroachDB. I also wasn't sure if the details that the Consul implementation was hiding were actually important.
- deleted 10y ago[deleted]
- harlowja 10y agoDo you (or people you know?) plan on publishing peer reviewed papers for how the lease algorithm works, how the multi-version concurrency control model works (and so on)? None of these are afaik things built in to raft but are add-ons that etcd has created (that may or may not even use raft). It'd be great to instill confidence in these add-on features by having them peer-reviewed in a similar manner as raft is/was/has been.
- deleted 10y ago[deleted]
- sciurus 10y agoZookeeper does not use Paxos. It uses its own protocol, Zab. https://cwiki.apache.org/confluence/display/ZOOKEEPER/Zab+vs.+Paxos https://cwiki.apache.org/confluence/display/ZOOKEEPER/Zab+vs...