There's an easy to understand visualisation of distributed consensus (specifically the Raft algorithm) here: http://thesecretlivesofdata.com/raft/
[deleted]
Flexible Paxos: Quorum intersection revisited
11–15 of 15 posts
Re: Flexible Paxos: Quorum intersection revisited
#12Earlier quoted context omitted.
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/b40971e7…
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 pr…
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-E...
Re: Flexible Paxos: Quorum intersection revisited
#13Not a paper, but I liked this related article https://news.ycombinator.com/item?id=11813180
Re: Flexible Paxos: Quorum intersection revisited
#14TL;DR summary (to my understanding, no sane human can ever claim it can summarize Paxos): The claim is that, once a leader is elected (ie. Q1), is no longer necessary to attain a majority quorum for actually accepting writes (ie. Q2). A minority quorum can accept writes, provided the minority contains at least one node that participated in the leader election. By increasing the leader election quorum number to higher…
Lamport can probably claim to summarize it as well as anyone: http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
Re: Flexible Paxos: Quorum intersection revisited
#15Earlier quoted context omitted.
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/b40971e7…
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 pr…
It is appropriate that Lamport's tool is being used to prove the correctness to an improvement of Lamport's algorithm.