4 ms·

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 tes

by jodah 11y ago

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 https://github.com/atomix/atomix-jepsen [2] https://www.datastax.com/dev/blog/testing-apache-cassandra-with-jepsen https://www.datastax.com/dev/blog/testing-apache-cassandra-w... [3] https://foundationdb.com/blog/call-me-maybe-foundationdb-vs-jepsen https://foundationdb.com/blog/call-me-maybe-foundationdb-vs-...

antirez 11y ago
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.
- jodah 11y ago
  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.md https://github.com/aphyr/jepsen/blob/master/doc/scaffolding....
takeda 11y ago
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 https://www.consul.io/docs/internals/jepsen.html [2] https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul
- aidenn0 11y ago
  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.

by jodah 11y ago

antirez 11y ago

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.

jodah 11y ago
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.md https://github.com/aphyr/jepsen/blob/master/doc/scaffolding....

takeda 11y ago

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 https://www.consul.io/docs/internals/jepsen.html [2] https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul

aidenn0 11y ago
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.