Millions of Tiny Databases
blog.acolyer.org
blog.acolyer.org
You're not getting rid of implementation bugs with TLA+, but it's a huge breath of fresh air as a formal documentation language.
Yeah! When I started with TLA+ I was mostly enamored with model checking and proofs. Those turned out to be useful, but the unexpected use of being a really great way to write crisp descriptions of protocols and algorithms is probably a bigger benefit. That's one of the reasons I tend to choose PlusCal over "raw" TLA+ these days: it's easier for others to read and engage with.
After publishing this paper, I had a great email conversation with Leslie Lamport about this use of TLA+. We talked about TLA+'s use as a "low ambiguity documentation" tool, and some of the cases where we've been able to resolve conversations about ambiguities in our implementation because we had the TLA+ spec to fall back on.
I'm quite partial to just using straight TLA+ for everything because it's both what ultimately it all desugars to anyway and because it makes what you put in TLC and what you write for your spec the same language. Plus once you're in the mindset of TLA+, the syntax of PlusCal has always seemed more of a distraction than anything else, but it does seem that PlusCal is a lot less scary for an experienced developer with no TLA+ experience.
Mostly the tradeoffs are the ones you mentioned. If I was the only audience of what I was writing, I’d pick TLA+ every time, but for a broader audience PlusCal can make this stuff much more approachable.
Parts of this blog post also align well with another recent post: Simple Systems Have Less Downtime[2]:
[1] https://github.blog/2018-10-30-oct21-post-incident-analysis/ [2] https://news.ycombinator.com/item?id=22471355
/s
This is an excellent model to have for high-reliability work. There are going to be failures, so the design should provide means of containing the failures.
The paper is also good at recognising the risk of cascade failures in failover systems, where a single excessive load causes a failure - but the process of trying to move the load elsewhere also becomes overloaded.
As the authors themselves point out, none of the fundamental building blocks of this system are particularly new. For example, the idea of partitioning a very large dataset into lots of independent slices, each of which is handled by its own Paxos group, is the same idea that forms the basis of Google's Megastore and Spanner, the former of which is more than a decade old.
Most of the interesting stuff in this paper is the discussion of the nuts-and-bolts of software engineering, such as testing, deployment and monitoring.
For open source solutions, BeeGFS.
If you want to pay and you are IBM fan, GPFS.