3 ms·
Amazing 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
by r0naa 11y ago
Amazing 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-easily-as-a-model-checker 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/ 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+.
- ahelwer 11y agoTLA+ 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.
- r0naa 11y agoRight, I have edited my original comment.
- dougws 11y agoHey, 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/ http://homes.cs.washington.edu/~jrw12/), and the other folks listed on our web page at http://verdi.uwplse.org/ http://verdi.uwplse.org/
- r0naa 11y agoApologies to your research partner for leaving him out, it's edited! Congratulations on the proof by the way, I am looking forward to this week-end so I can have some time to appreciate it with more depth! :-)
- dougws 11y agoThanks! Let us know if you have any questions about the proof itself--unfortunately, it's not particularly well-documented, and Coq isn't super easy to read in the first place.
- notsony 11y agoCan you recommend and (1) books and (2) online lectures/courses on proofs which use Coq? Thanks!
- dougws 11y agoAt this point, the standard intro text is Software Foundations [1]. I highly recommend it; it will teach you Coq and also probably make you a better programmer. After SF, Certified Programming with Dependent Types [2] gets more into the practice of proving serious programs correct. These books are both available online in the form of literate Coq files. As far as online lectures, OPLSS [3] often has Coq lectures which are quite good. [1] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html [2] http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ [3] https://www.cs.uoregon.edu/research/summerschool/summer15/ https://www.cs.uoregon.edu/research/summerschool/summer15/
- notsony 11y agoThanks!
- deleted 11y ago[deleted]