I share interesting articles, videos, papers and more about distributed systems, formal methods and computer science.
In an earlier post I argued that coordination is about ruling out futures that the world hasn't ruled out on its own. Waiting, ordering, and commitment all…
In our services ecosystem it’s usually the case that services can handle a limited amount of requests per second. We show how we introduced a new algorithm for our publish-subscribe queue system. The road to production deployment highlights some key distributed systems’ takeaways we’d like to discuss.
How ClickHouse Cloud's two-window recommender and target-tracking CPU algorithm cut scale-down latency from 30 hours to 3 hours while eliminating oscillations and reducing infrastructure costs.
I get a lot of emails from people asking me how they can begin to learn the vast world of databases, and whether they are far enough along on their programming journey to bother trying to start to learn this sub-genre of CS. This post is meant to be my authoritative answer to those questions... Sort of a database specific version of: this post about programming in general.
This is the story of how a RocksDB unit test I added four years ago, a mini-stress test you might call it, revealed a novel hardware bug in a newer CPU. It w...
Three Sets of Specs (for Staying in Spec) In the last post I talked about how systems formalisms are like sculpting with a chisel: we remove behaviors we don’t…
I have an early adulthood trauma from struggling to understand consensus amidst a myriad of poor explanations. I am overcompensating for that by adding my own attempts to the fray. Today, I want to draw a series of pictures which could be helpful. You can see this post as a set of missing illustrations for Notes on Paxos, or, alternatively, you can view that post as a more formal narrative counter-part for the present one.
why compression is (almost) always worthwhile
Learn how we used modular protocol specification for verifying both correctness and performance of MongoDB’s distributed transactions protocol.
We can automatically check correctness properties of a TLA+ specification using TLC, a model checker that will exhaustively explore a spec’s reachable states...
