Is Redlock Safe? Reply to Redlock Analysis

Re:Is Redlock Safe? Reply to Redlock Analysis by jodah on Tuesday February 09, 2016 @11:41AM (#11066534)

The article calls on someone(?) to Jepsen test Redlock, which is a good idea, but I think that the author(s) of such systems should release their own Jepsen test suite along with the software they're purporting to be safe (as others have done [1][2][3]). I would suspect that operations on Redlock, when subjected to nemesis that partition, kill and skew-clocks on various nodes, would not be found linearizable.

In general, I don't understand why one would build a system that attempts to approximate consensus without just using one of the proven consensus algorithms. Redlock is not the only one here, there are other systems that do this as well.

[1] https://github.com/atomix/atomix-jepsen

[2] https://www.datastax.com/dev/blog/testing-apache-cassandra-w...

[3] https://foundationdb.com/blog/call-me-maybe-foundationdb-vs-...

[ Parent | on HN ]

Re:Is Redlock Safe? Reply to Redlock Analysis by takeda on Tuesday February 09, 2016 @02:20PM (#11067925)

The problem with Jepsen is that it can prove that systems are unsafe, but it can't be used to prove that systems are safe.

For example Consul did their own Jepsen testing[1] in which they passed them, but Kyle pointed out [2] that they passed them only because they changed timeouts from 1 s to 300 ms effectively making the race condition window smaller.

[1] https://www.consul.io/docs/internals/jepsen.html [2] https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul

[ Parent | on HN ]

Re:Is Redlock Safe? Reply to Redlock Analysis by aidenn0 on Tuesday February 09, 2016 @07:02PM (#11069839)

It's typicaly not tractable to prove that a system is safe. For example, RethinkDB used the raft consensus algorithm, which on its own is proven correct, but due to a bug could in some cases break linearization. Jepsen was able to uncover this.

The best method we currently have for demonstrating that large systems are safe is to try really hard to prove that they are unsafe and fail.

[ Parent | on HN ]

Re:Is Redlock Safe? Reply to Redlock Analysis by antirez on Tuesday February 09, 2016 @12:20PM (#11066913)

Redlock has nothing to do with linearizability. The only strong property it tries to provide is mutual exclusivity. I'm interested in working to a Jepsen test for this, but the Jepsen learning curve and actual level of documentation requires to spend a lot of time on writing the test.

[ Parent | on HN ]

Re:Is Redlock Safe? Reply to Redlock Analysis by jodah on Tuesday February 09, 2016 @12:54PM (#11067191)

I'm not sure that merely checking the result of some set of operations - whether a mutex is held by the expected process - tells you very much about the validity of how that mutex was obtained (assuming interleaving requests and such). This is where you need to explore the history, which is what the linearizability checker does and which is what Jepsen tests generally use.

It is a bit of work and learning curve writing a Jepsen test suite, but it's not too bad, particularly with the excellent docs that Kyle has recently written:

https://github.com/aphyr/jepsen/blob/master/doc/scaffolding....

[ Parent | on HN ]