3 ms·
Nice writeup. Complex protocol like this always makes me wonder, how do people even test it?
by eva1984 11y ago
Nice writeup. Complex protocol like this always makes me wonder, how do people even test it?
- gioele 11y agoThey have these things called "proofs": http://cstheory.stackexchange.com/questions/25851/correctness-proofs-of-classic-paxos-and-fast-paxos http://cstheory.stackexchange.com/questions/25851/correctnes... Jokes aside, there are two ways out: huge simulators or writing very very simple code that matches 1-to-1 the steps of the proof. And Lamport's writing style for proofs [1] lends itself to simple matching implementations. [1] "How to Write a 21st Century Proof" http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
- krenoten 11y agoTLA+ model checking and an implementation that follows the spec as closely as possible.
- felixgallo 11y agojepsen, quickcheck, interleave testers like concuerror; or, by implementing directly in a proof assistant/language like coq, as was recently done with raft.