3 ms·

Have you read this Salvatore? http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/

Have you read this Salvatore? http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo... > ... The good thing is that distributed systems are, unlike other fields of programming, pretty mathematically exact, or they are not, so a given set of properties can be guaranteed by an algorithm or the algorithm may fail to guarantee them under certain assumptions. In this analysis I’ll analyze .. Saw no mathematics in your article.

jpgvm 11y ago
More important than that paper are the rest of the papers by Leslie Lamport. Specifically the paper entitled Time, Clocks and the Ordering of Events in a Distributed System. [1] This is basically the seminal paper on distributed systems and should be required reading for anyone considering playing with distributed locking mechanisms. [1] http://research.microsoft.com/en-us/um/people/lamport/pubs/time-clocks.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/t...
- eternalban 11y ago
  The paper discusses benefits of applying the theoretical tools and written by engineers. You[r] cite is of course essential but no doubt OP knows this as well :)
  - jpgvm 11y ago
    Very true, I didn't consider it like that.
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 ago
  I'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 ago
  So 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.
dwenzek 11y ago
Before any proof, the debate would benefit from more precise definitions. For instance, the issue around the usage of fencing tokens to reject any late usage of a lock is unclear just because the protected resource and its access are themselves unspecified. Is the resource distributed or not? If distributed, does the resource has a mean to ensure that tokens are increasing over all the nodes? Does the resource have a mean to rollback any effects done by a client which session is interrupted by a timeout? Likewise for the timing arguments. It seems clear to everyone that timeouts provide only some protection rather than a guarantee. A more precise timeline of the worst case scenario will help to estimate that protection given the misc timeout values and clock shifts.

jpgvm 11y ago

More important than that paper are the rest of the papers by Leslie Lamport. Specifically the paper entitled Time, Clocks and the Ordering of Events in a Distributed System. [1] This is basically the seminal paper on distributed systems and should be required reading for anyone considering playing with distributed locking mechanisms. [1] http://research.microsoft.com/en-us/um/people/lamport/pubs/time-clocks.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/t...

eternalban 11y ago
The paper discusses benefits of applying the theoretical tools and written by engineers. You[r] cite is of course essential but no doubt OP knows this as well :)
- jpgvm 11y ago
  Very true, I didn't consider it like that.

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 ago
I'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 ago
So 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.

dwenzek 11y ago

Before any proof, the debate would benefit from more precise definitions. For instance, the issue around the usage of fencing tokens to reject any late usage of a lock is unclear just because the protected resource and its access are themselves unspecified. Is the resource distributed or not? If distributed, does the resource has a mean to ensure that tokens are increasing over all the nodes? Does the resource have a mean to rollback any effects done by a client which session is interrupted by a timeout? Likewise for the timing arguments. It seems clear to everyone that timeouts provide only some protection rather than a guarantee. A more precise timeline of the worst case scenario will help to estimate that protection given the misc timeout values and clock shifts.