11–20 of 30 posts
Questions for the researchers, if they are reading:
- Does this proof cover any liveness concerns (weak fairness, deadlock freedom, etc) in addition to the safety property of linearizability?
- If not, what would it take to extend this model to cover liveness? Is this even a good starting point?
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…
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/
Extremely cool stuff. Questions for the researchers, if they are reading: - Does this proof cover any liveness concerns (weak fairness, deadlock freedom, etc) in addition to the safety property of linearizability? - If not, what would it take to extend this model to cover liveness? Is this even a good starting point?
As you probably know, Raft and other consensus algorithms are not guaranteed to be live in all situations. But subject to some assumptions about the frequency of failure, they are guaranteed to make progress.
In Verdi, systems are verified with respect to semantics for the network they are running on. Our semantics currently don't include any restrictions about how often failures can happen; a failure "step" can occur at any time. We're not sure what the best way is to introduce this kind of restriction, but we've got a couple ideas. One would be to guarantee that the total number of failures has some finite bound which is unknown to the system itself but which is available during verification. Another would be to model failure probabilistically. We will probably end up doing at least one of these things in the next year or so :).
Earlier quoted context omitted.
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/
Apologies 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! :-)
Extremely cool stuff. Questions for the researchers, if they are reading: - Does this proof cover any liveness concerns (weak fairness, deadlock freedom, etc) in addition to the safety property of linearizability? - If not, what would it take to extend this model to cover liveness? Is this even a good starting point?
We are reading! This is a great question. We currently don't prove anything about liveness. We'd love to work on this. As you probably know, Raft and other consensus algorithms are not guaranteed to be live in all situations. But subject to some assumptions about the frequency of failure, they are guaranteed to make progress. In Verdi, systems are verified with respect to semantics for the network they are running on…
Earlier quoted context omitted.
Apologies 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! :-)
Thanks! 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.
Earlier quoted context omitted.
Kyle Kingsbury has a good look at linearizability and other forms of consistency: https://aphyr.com/posts/313-strong-consistency-models
That was a great read. Thanks for a new blog to put on my RSS feed
Earlier quoted context omitted.
Thanks! 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.
Can you recommend and (1) books and (2) online lectures/courses on proofs which use Coq? Thanks!
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
[2] http://adam.chlipala.net/cpdt/
[3] https://www.cs.uoregon.edu/research/summerschool/summer15/
Earlier quoted context omitted.
Apologies 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! :-)
Thanks! 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.