https://github.com/uwplse/verdi/pull/16 … only 18 months in the making.
-
@wilcoxjay can you say a little more about what's done?
@ongardie we have implemented Raft in Coq's functional language and proved it linearizable wrt the underlying state machine
-
-
@ongardie this includes verifying the five properties from the paper as well as some additional things about responses to clientsThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@ongardie we prove this wrt a model of the environment that can dup, drop, and reorder msgs, as well as crash and reboot nodes -
@wilcoxjay that's awesome. "thanks for taking this on" doesn't feel like enough
End of conversation
New conversation -
-
-
@ongardie it's important to note that we don't verify liveness, only safety properties. So it's possible that our implementation could hang -
Tweet unavailable
-
@palvaro totally. but safe algorithms that make absolutely no progress guarantees aren't worth much. so we'd like to prove *something*
-
Tweet unavailable
-
@palvaro staggering naivety and lots of beer
End of conversation
New conversation -
-
-
@ongardie we also don't implement all features of a production system. for example, we don't do log compaction (yet!) -
@wilcoxjay you guys should have made a documentary -
@ongardie that would consist mostly of swearing and banging head on desk -
@wilcoxjay ha, I'd watch it still
End of conversation
New conversation -
-
-
@wilcoxjay so that's it then. You win.Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.