3 ms·
Unfortunately to test Redlock with a formal method is pretty useless. The algorithm is so trivial, for the part you can mathematically model it, that is a waste
by antirez 11y ago
Unfortunately to test Redlock with a formal method is pretty useless. The algorithm is so trivial, for the part you can mathematically model it, that is a wasted effort to model it: even with a proof of the lock acquisition process it all boils down to "is the system model credible"? And that's what we are debating. Note that similarly Martin don't even try to address the problem of how the lock is acquired for the same reason I guess. Also note that if you try to model the problem adding unbound processes pauses, and put as a requirement mutual exclusivity with auto-release, I don't think there is a way the model will ever be validated, whatever system you model implementing this.
- agentultra 11y agoI'm still relatively new to formal specification but it seems that some form of weak/strong fairness would suffice for the correctness of your invariant and then it's a matter of testing your liveness properties while holding the invariant with a model checker. TLA+ seems pretty good at this. Why would this be a waste of effort?
- sseveran 11y agoSo since it depends on the correctness of the underlying system is there a TLA+ (or other) proof for that? Last time jepsen ran on redis it showed that it was broken unless something has changed in the meantime.