Hacker News Reader

Comment by agentultra | Hacker News Reader

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.

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

[1] http://www-users.cselabs.umn.edu/classes/Spring-2016/csci821...

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

I 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 :) )

In Haskell, I presume? Will it be open sourced? :)

Actually doing in Agda first. Coinductive programming is a delight with Agda 2.5.

But yes that's the plan.

Consul's Raft implementation is leagues better than etcd's, unfortunately.

Is that still the case with Etcd v3? I remember reading somewhere that they were rewriting the Raft implementation in Etcd a good while ago.

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

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

It's based on Raft : https://github.com/coreos/etcd/tree/master/raft

https://raft.github.io/

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

Zookeeper does not use Paxos. It uses its own protocol, Zab.

https://cwiki.apache.org/confluence/display/ZOOKEEPER/Zab+vs...

Reply on news.ycombinator.com