5 ms·

one more difference I would add is how a leader is elected in Raft (randomized) vs VSR (deterministic succession)

jorangreef 1y ago
Yes, exactly. That difference came in with '12 VSR's view change (deterministic, round-robin), which upgraded '88 VSR's view change. '14 Raft missed this upgrade, unfortunately (despite citing the '12 paper), thus preserving Oki's '88 "pick the candidate with longest log". I find the history of consensus fascinating, and was fortunate to interview both Brian Oki and James Cowling (so many anecdotes): https://www.youtube.com/watch?v=ps106zjmjhw https://www.youtube.com/watch?v=ps106zjmjhw
- ingloriousB 1y ago
  The Raft authors didn't "miss" it, they just decided that randomized was simpler--and simplicity was a deliberate design goal. They found randomized was easier to reason about compared to trying to figure out how to explain and prove correctness when the next "determined" leader has died or been partitioned. Lacking formal methods, the original VSR work seems less rigorous/proven. Maybe rigorous proof was just not possible at the time; after all Lamport had to work really hard to prove Paxos correct. Consider that page 31 of Brian Oki's dissertation, http://www.pmg.csail.mit.edu/papers/MIT-LCS-TR-423.pdf http://www.pmg.csail.mit.edu/papers/MIT-LCS-TR-423.pdf , he complete misses problem that is discussed in Figure 3.7 of the Raft dissertation. That is, the "new view" may be missing information from a leader who had a higher term/view number, but is temporarily offline. Does the orignal VSR provide the same fix that Raft does for that scenario? Does it address other possible scenarios? Mechanical proofs seem conspicuously absent, and even human proofs aren't in ready evidence.
  - jorangreef 1y ago
    > “seems” / “seem” Are you intending to suggest there are no formal proofs since? For example, you compare ‘14 Raft against ‘88 VSR, ignoring the interim progress made by MIT with ‘12 VSR? It would seem fair to compare the latest version of both, no?
    - ingloriousB 1y ago
      :) I'm only using "seem" to indicate the limits of my knowledge. I was just hoping someone would chime in with a link to stronger/formal proof for VSR. Are you aware of any? So, yes, to my limited knowledge, I've not found any existing formal proofs for VSR. The 2012 VSR revisited clearly labels their arguments informal; in section 8: "In this section we provide an informal discussion of the correctness of the protocol." I'd be delighted to learn of any formal / machine checked proofs of VSR ; equivalent to the Verdi project for Raft. These are elaborate and subtle protocols, easy to get wrong. In particular when it comes to things like reconfiguration, even Raft had the famous 2016 bug in the simpler of its two reconfiguration protocols. Note that Verdi did not attempt to verify the reconfiguration protocol; apparently it was too difficult. There was an attempt earlier this year to give a proven reconfiguration protocol for Raft called Recraft[1], based on an earlier paper called Adore[2]. They discuss why reconfiguration is so difficult to prove. It has to do with circularity. "ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol" by Kezhi Xiong, Soonwon Moon, Joshua Kang, Bryant Curto, Jieung Kim, Ji-Yong Shin. last revised 28 Apr 2025, v2. [1] https://arxiv.org/abs/2504.14802 https://arxiv.org/abs/2504.14802 [2] https://dl.acm.org/doi/pdf/10.1145/3519939.3523444 https://dl.acm.org/doi/pdf/10.1145/3519939.3523444 I'm not completely convinced yet that ReCraft works; at one point I thought they assumed away certain scenarios -- but I need to revisit it with a close reading. At a minimum, reading the Adore paper's discussion of how much subtlety is involved is pretty compelling. My conclusion is that formal proof is an absolute necessity to have a fighting chance at a correct implementation--especially when it comes to reconfiguration.
      - jorangreef 1y ago
        There are at least two formal proofs. Have you tried Googling for them, instead of creating a throwaway account to comment anonymously here? :)
        ingloriousB 1y ago
        Per the site guidelines[1], please avoid gratuitous negativity. [1] https://www.ycombinator.com/blog/new-hacker-news-guideline https://www.ycombinator.com/blog/new-hacker-news-guideline > https://www.ycombinator.com/blog/new-hacker-news-guideline https://www.ycombinator.com/blog/new-hacker-news-guideline Certainly I've googled. I have found no proofs. Surely by now you would actually exhibit the formal proof if you had one right? (He asks, for the 3rd time). Note that a TLA+ spec is not a formal proof. Also note that a model checking run is not a formal proof. I'm still hoping to learn something new about how proven is, say, the reconfiguration or recovery protocols in VSR. So far I can only conclude that my research has turned up nothing as far a formal proof for VSR. Please show me I'm wrong with a link to one. :)

Yes, exactly. That difference came in with '12 VSR's view change (deterministic, round-robin), which upgraded '88 VSR's view change. '14 Raft missed this upgrade, unfortunately (despite citing the '12 paper), thus preserving Oki's '88 "pick the candidate with longest log". I find the history of consensus fascinating, and was fortunate to interview both Brian Oki and James Cowling (so many anecdotes): https://www.youtube.com/watch?v=ps106zjmjhw https://www.youtube.com/watch?v=ps106zjmjhw

ingloriousB 1y ago
The Raft authors didn't "miss" it, they just decided that randomized was simpler--and simplicity was a deliberate design goal. They found randomized was easier to reason about compared to trying to figure out how to explain and prove correctness when the next "determined" leader has died or been partitioned. Lacking formal methods, the original VSR work seems less rigorous/proven. Maybe rigorous proof was just not possible at the time; after all Lamport had to work really hard to prove Paxos correct. Consider that page 31 of Brian Oki's dissertation, http://www.pmg.csail.mit.edu/papers/MIT-LCS-TR-423.pdf http://www.pmg.csail.mit.edu/papers/MIT-LCS-TR-423.pdf , he complete misses problem that is discussed in Figure 3.7 of the Raft dissertation. That is, the "new view" may be missing information from a leader who had a higher term/view number, but is temporarily offline. Does the orignal VSR provide the same fix that Raft does for that scenario? Does it address other possible scenarios? Mechanical proofs seem conspicuously absent, and even human proofs aren't in ready evidence.
- jorangreef 1y ago
  > “seems” / “seem” Are you intending to suggest there are no formal proofs since? For example, you compare ‘14 Raft against ‘88 VSR, ignoring the interim progress made by MIT with ‘12 VSR? It would seem fair to compare the latest version of both, no?
  - ingloriousB 1y ago
    :) I'm only using "seem" to indicate the limits of my knowledge. I was just hoping someone would chime in with a link to stronger/formal proof for VSR. Are you aware of any? So, yes, to my limited knowledge, I've not found any existing formal proofs for VSR. The 2012 VSR revisited clearly labels their arguments informal; in section 8: "In this section we provide an informal discussion of the correctness of the protocol." I'd be delighted to learn of any formal / machine checked proofs of VSR ; equivalent to the Verdi project for Raft. These are elaborate and subtle protocols, easy to get wrong. In particular when it comes to things like reconfiguration, even Raft had the famous 2016 bug in the simpler of its two reconfiguration protocols. Note that Verdi did not attempt to verify the reconfiguration protocol; apparently it was too difficult. There was an attempt earlier this year to give a proven reconfiguration protocol for Raft called Recraft[1], based on an earlier paper called Adore[2]. They discuss why reconfiguration is so difficult to prove. It has to do with circularity. "ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol" by Kezhi Xiong, Soonwon Moon, Joshua Kang, Bryant Curto, Jieung Kim, Ji-Yong Shin. last revised 28 Apr 2025, v2. [1] https://arxiv.org/abs/2504.14802 https://arxiv.org/abs/2504.14802 [2] https://dl.acm.org/doi/pdf/10.1145/3519939.3523444 https://dl.acm.org/doi/pdf/10.1145/3519939.3523444 I'm not completely convinced yet that ReCraft works; at one point I thought they assumed away certain scenarios -- but I need to revisit it with a close reading. At a minimum, reading the Adore paper's discussion of how much subtlety is involved is pretty compelling. My conclusion is that formal proof is an absolute necessity to have a fighting chance at a correct implementation--especially when it comes to reconfiguration.
    - jorangreef 1y ago
      There are at least two formal proofs. Have you tried Googling for them, instead of creating a throwaway account to comment anonymously here? :)
      - ingloriousB 1y ago
        Per the site guidelines[1], please avoid gratuitous negativity. [1] https://www.ycombinator.com/blog/new-hacker-news-guideline https://www.ycombinator.com/blog/new-hacker-news-guideline > https://www.ycombinator.com/blog/new-hacker-news-guideline https://www.ycombinator.com/blog/new-hacker-news-guideline Certainly I've googled. I have found no proofs. Surely by now you would actually exhibit the formal proof if you had one right? (He asks, for the 3rd time). Note that a TLA+ spec is not a formal proof. Also note that a model checking run is not a formal proof. I'm still hoping to learn something new about how proven is, say, the reconfiguration or recovery protocols in VSR. So far I can only conclude that my research has turned up nothing as far a formal proof for VSR. Please show me I'm wrong with a link to one. :)