3 ms·
Very interesting writeup. Did you consider using formal verification tools such as the TLA family to ensure that your sync protocol is well-specified and consi
by jhayward 7y ago
Very interesting writeup. Did you consider using formal verification tools such as the TLA family to ensure that your sync protocol is well-specified and consistent?
- sujayakar 7y agoyeah, I'm familiar with those tools, and other teams at dropbox have used TLA+ for verifying their protocols, but we haven't done it for our system yet. we've spent most of our time on testing working on better randomized testing, with the idea that covering more surface area there has higher ROI. but I can definitely see value there, especially once the protocol "settles down" and sees less change over time.