Prove Raft Correct
github.com
Prove Raft Correct
1–10 of 30 posts
Re: Prove Raft Correct
#2Amazing job! It has been mentioned on the Raft mailing list that a proof was in a progress, but to be honest I did not expect anything to come up before a year or so. Forgive my lack of faith! :-)
Well done!
edit: to provide some context
- Raft is a distributed consensus algorithm that is seen by many as a viable alternative to *-Paxos because of its relative simplicity. It was created by D. Ongaro and J. Ousterhout (Tcl/Tk!)
- D. Ongaro's dissertation includes a TLA+ specifications of Raft; TLA+ is a model checker (see ) for a more detailed explanation of what is a model checker/theorem prover's job
- TLA+ is a model checker; Coq is a proof assistant. See https://stackoverflow.com/questions/22418448/can-coq-be-used... for a more detailed explanation.
- Verdi is a Coq framework to make formal proof about distributed systems.
- Doug Woos and James Wilcox, made a proof of Raft using Verdi; Verdi helps you figure whether your implementation of X (in this case X=Raft) meets the specifications (Leader Safety, strong consistency etc..)
Link to the Verdi website: http://verdi.uwplse.org/
edit: as noted by ahelwer, TLA+ is not a model checker but a language to describe a distributed system's specifications. I was referring to TLC which can work with TLA+.
Re: Prove Raft Correct
#3What exactly is a consensus algorithm and how do you prove linearizability?
Re: Prove Raft Correct
#4Amazing job! It has been mentioned on the Raft mailing list that a proof was in a progress, but to be honest I did not expect anything to come up before a year or so. Forgive my lack of faith! :-) Well done! edit: to provide some context - Raft is a distributed consensus algorithm that is seen by many as a viable alternative to *-Paxos because of its relative simplicity. It was created by D. Ongaro and J. Ousterhout…
TLA+ is a formal specification language, not a model checker. There exists a model checker called TLC which works with TLA+. There also exists an associated proof system called TLAPS; TLAPS has been used to formally prove correctness of Byzantine Paxos.
Re: Prove Raft Correct
#5Amazing job! It has been mentioned on the Raft mailing list that a proof was in a progress, but to be honest I did not expect anything to come up before a year or so. Forgive my lack of faith! :-) Well done! edit: to provide some context - Raft is a distributed consensus algorithm that is seen by many as a viable alternative to *-Paxos because of its relative simplicity. It was created by D. Ongaro and J. Ousterhout…
Hey, I'm Doug Woos--thanks for this excellent summary! It's worth noting that the Raft proof was completed by a team of people, including me, my research partner James Wilcox (http://homes.cs.washington.edu/~jrw12/), and the other folks listed on our web page at http://verdi.uwplse.org/
Re: Prove Raft Correct
#6What exactly is a consensus algorithm and how do you prove linearizability?
distributed consensus is about having a group of processes agree on a single data value. For example, imagine you have a cluster of server. Each node has a replicated database.
(1) You want all your nodes to have the exact same replica of the database i.e consistency across your cluster.
You would need to reach consensus before any node actually adds anything to its local database to make sure that property (1) is fulfilled.
== Linearizability is just a consistency model i.e a variant of property 1 with stronger/weaker constraints.
Re: Prove Raft Correct
#7What exactly is a consensus algorithm and how do you prove linearizability?
distributed consensus is about having a group of processes agree on a single data value. For example, imagine you have a cluster of server. Each node has a replicated database. (1) You want all your nodes to have the exact same replica of the database i.e consistency across your cluster. You would need to reach consensus before any node actually adds anything to its local database to make sure that property (1) is fu…
Oh wow, that's actually really powerful stuff! Thanks for the explanation.
Re: Prove Raft Correct
#8Amazing job! It has been mentioned on the Raft mailing list that a proof was in a progress, but to be honest I did not expect anything to come up before a year or so. Forgive my lack of faith! :-) Well done! edit: to provide some context - Raft is a distributed consensus algorithm that is seen by many as a viable alternative to *-Paxos because of its relative simplicity. It was created by D. Ongaro and J. Ousterhout…
TLA+ is a formal specification language, not a model checker. There exists a model checker called TLC which works with TLA+. There also exists an associated proof system called TLAPS; TLAPS has been used to formally prove correctness of Byzantine Paxos.
Right, I have edited my original comment.
Re: Prove Raft Correct
#9What exactly is a consensus algorithm and how do you prove linearizability?
Kyle Kingsbury has a good look at linearizability and other forms of consistency: https://aphyr.com/posts/313-strong-consistency-models
Re: Prove Raft Correct
#10What exactly is a consensus algorithm and how do you prove linearizability?
Kyle Kingsbury has a good look at linearizability and other forms of consistency: https://aphyr.com/posts/313-strong-consistency-models
Kyle Kingsbury is the man, and his blog is a must read to anyone interested/curious by distributed systems.