Hacker News Reader

Comment by justinsb | Hacker News Reader

As with all distributed systems algorithms, we should assume Redlock is unsafe until proven otherwise. A proof looks like http://ramcloud.stanford.edu/raft.pdf (Raft), http://research.microsoft.com/en-us/um/people/lamport/pubs/p... (Paxos) or http://www.tcs.hut.fi/Studies/T-79.5001/reports/2012-deSouza... (Zookeeper).

Personally I'd prefer stronger proofs than even those, but I think those papers get us to the point where implementation issues are as important as theoretical issues.

In my personal opinion, Redlock is not at the point where we even need to consider the implementation.

View on HN

A good starting point. But those proofs are notoriously based on fairy tales such as reliable networking, Fail/Stop, and other white lies.

The fact that a protocol (e.g. Raft) has been proven correct sets the floor but it is certainly not sufficient to assume correctness of an implementation.

It should always be a prerequisite to have a proof before one begins an implementation. If one cannot construct such a proof then they have no business trying to design new distributed algorithms. Fortunately there are a few algorithms for proofs of replicated state machines available as previously noted.

Proofs will typically show the limitations of an algorithm, for instance the original paxos paper notes that the contained algorithm does not provide liveliness.

A system based on an algorithm with a proof has some chance of being correct, while a system based on an algorithm with no proof while technically it may have a non-zero probability of being correct that probability approaches zero.

Having worked on such systems and having talked to some people who have worked on debugging issues with paxos implementations at extreme scale while it is virtually impossible to to ensure that the system will be able to make forward progress it is possible to ensure that the state of the state machine remains correct.

When I look at an implementation of such an algorithm to evaluate it I pay very careful attention to the test suites. The more bizarre the tests they contain the more likely the implementation is to handle very weird network edge cases.

> those proofs are notoriously based on fairy tales such as reliable networking

Raft isn't. (I actually don't believe Paxos or Zookeeper do either, but I only understand Raft, so let me speak for that one.) Directly from the link in the post you're responding to:

> Consensus algorithms for practical systems typically have the following properties:

> They ensure safety (never returning an incorrect result) under all non-Byzantine conditions, including network delays, partitions, and packet loss, duplication, and reordering.

This applies to Raft, as well: Raft-the-algorithm will behave correctly during these events. The paper linked to above provides a proof of such.

> The fact that a protocol (e.g. Raft) has been proven correct sets the floor but it is certainly not sufficient to assume correctness of an implementation.

These are two separate things, and you need both. You need to know that an algorithm is sound, that it accomplishes what it sets out to do. You also need to know that a particular implementation of an algorithm is correct.

(While I said I haven't read the ZK paper, it does mention,

> Paxos does not require FIFO channels for communication, so it tolerates message loss and reordering.

)

> is certainly not sufficient to assume correctness of an implementation

Indeed. This is where tools like Jepsen and good fuzz testing can help.

The algorithm needs a proof and the implementation needs rigorous testing (Jepsen).

Reply on news.ycombinator.com