4 ms·

If your summary is accurate (haven't read the paper yet), I don't think this works, because if you don't have a proper quorum, you can't know that the leader is

by btrask 10y ago

If your summary is accurate (haven't read the paper yet), I don't think this works, because if you don't have a proper quorum, you can't know that the leader is still valid at the time of an event. It might've been re-elected in the meanwhile. The only way to know is to "check in" with all the other nodes. I recently proposed this idea (informally) and had to retract it: https://bentrask.com/?q=hash://sha256/b40971e7b30324fdda15ce03 https://bentrask.com/?q=hash://sha256/b40971e7b30324fdda15ce... Disclaimer: totally not an expert.

jlouis 10y ago
The nice thing about the paper is that it is transparent. It includes a TLA+ specification for the claims that they make. In turn, you have a concrete model checked implementation you can talk about or use a basis for understanding where either their or your proposed idea either holds or fails. Note that a model can specify the wrong correctness criterion in practice. So you may have a "proof" which works, yet the proposition proven is wrong. In general, when working on distributed systems, we usually want some kind of formal criterion of correctness. The failure modes of such system are quite hard to get right, and hence retractions of claims are plenty. Sadly, we have too little literature on how to on-board people on model checkers such as TLA+, proof assistants such as Coq, Isabelle/HOL or NuPRL, and QuickCheck systems such as Haskell or Erlang QuickCheck, Clojure's core.spec (I believe), etc.
- rusanu 10y ago
  Book recommendation: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [0]. I did read it, but unfortunately I can't say I actually understood it as in to be able to use it day-to-day. [0] https://www.amazon.ca/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X https://www.amazon.ca/Specifying-Systems-Language-Hardware-E...
- jpitz 10y ago
  It is appropriate that Lamport's tool is being used to prove the correctness to an improvement of Lamport's algorithm.

by btrask 10y ago

jlouis 10y ago

The nice thing about the paper is that it is transparent. It includes a TLA+ specification for the claims that they make. In turn, you have a concrete model checked implementation you can talk about or use a basis for understanding where either their or your proposed idea either holds or fails. Note that a model can specify the wrong correctness criterion in practice. So you may have a "proof" which works, yet the proposition proven is wrong. In general, when working on distributed systems, we usually want some kind of formal criterion of correctness. The failure modes of such system are quite hard to get right, and hence retractions of claims are plenty. Sadly, we have too little literature on how to on-board people on model checkers such as TLA+, proof assistants such as Coq, Isabelle/HOL or NuPRL, and QuickCheck systems such as Haskell or Erlang QuickCheck, Clojure's core.spec (I believe), etc.

rusanu 10y ago
Book recommendation: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [0]. I did read it, but unfortunately I can't say I actually understood it as in to be able to use it day-to-day. [0] https://www.amazon.ca/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X https://www.amazon.ca/Specifying-Systems-Language-Hardware-E...
jpitz 10y ago
It is appropriate that Lamport's tool is being used to prove the correctness to an improvement of Lamport's algorithm.