2 ms·
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 f
by 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 agoI'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....