mjb

9 ms·

61.
by mjb 2y ago
I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib ( https://github.com/leanprover-community/mathlib4 ). What’s so great
62.
by mjb 2y ago
> I'm surprised this is seen as a liability of mmap rather than a cooperative scheduler that isn't using native kernel threads Indeed. In practice, though, it's easier to write high performance servers and storage systems
63.
by mjb 2y ago
Modern data center networks offer RTTs about 100x lower than hard drive latency, and comparable to local SSD. It depends, of course, how far over the network you're going, and how fast the other side responds, but <100us is very ach
64.
by mjb 2y ago
I like this point - it's no secret that mmap can make memory access cost the same as an IO (swap can too) - but the interaction with async schedulers isn't immediately obvious. The cost can, sometimes, be even higher than this pos
65.
by mjb 2y ago
Super cool to see this here. If you're at all interested in big systems, you should read this. > Compounding this latency, hard drive performance is also variable depending on the other transactions in the queue. Smaller requests th
66.
by mjb 2y ago
Maybe what I should have said is "you can't just retry transactions against a strict serializable database and expect to still get strict serializability (from the applications's perspective)". This is true of distribute
67.
by mjb 2y ago
The first bug is a great reminder that even strict serializability doesn't imply idempotency. If you're doing non-idempotent operations like unconditional writes, you've got to think very carefully before you add any retries
68.
by mjb 2y ago
Good list! Some of my favorites: - The Shining Mountain by Pete Boardman (one of my favorite of all books, two pretty normal guys doing something absolutely epic) - Everest: The Cruel Way by Joe Tasker (maybe history's single greatest
69.
by mjb 2y ago
> One really wonders about the competence of the committee which was selecting climbers for the fatal attempt. That's not really what happened. There wasn't some committee deciding that Mallory and Irvine should go up that day
70.
by mjb 2y ago
I haven't read this one yet, it's on my list. If you're interested in learning a lot more about the background and context, I'd recommend: - "Into the Silence: The Great War, Mallory, and the Conquest of Everest&quo
71.
by mjb 2y ago
> And you can’t “automate” away the rare things, even the technical ones. By their nature they’re difficult to define, hence difficult to monitor, and difficult to repair without the forensic skills of a human engineer. There are two way
72.
by mjb 2y ago
Having multiple logical buckets per physical node doesn't fix this problem. It does help ensure that the bucket sizes are closer to uniform, but not that items hash uniformly into the available buckets. Even if all the buckets are exac
73.
by mjb 2y ago
This is a very cool page. I love little simulations like this for building intuition for systems problems. Practical systems deal with this by not caring strongly about overflow (caches), by running at low enough utilizations that overflow
74.
by mjb 2y ago
Java is uncool, and to some people there's nothing scarier than not looking cool. Java is great. Solid ecosystem, solid performance, decent memory safety story, tons of production experience, etc.
75.
by mjb 2y ago
Many performance-sensitive in-datacenter applications have moved away from TCP to reliable datagram protocols. Here's what that looks like at AWS: https://ieeexplore.ieee.org/document/9167399
76.
by mjb 2y ago
TCP_QUICKACK does fix the worst version of the problem, but doesn't fix the entire problem. Nagles algorithm will still wait for up to one round-trip time before sending data (at least as specified in the RFC), which is extra latency w
77.
by mjb 2y ago
> Crash-only software is actually more reliable because it takes into account from the beginning an unavoidable fact of computing - unexpected crashes. This is a critical point for reliable single-machine systems, and for reliable distri
78.
by mjb 2y ago
I use route53 for my site (brooker.co.za), and have had no complaints. Much nicer than dealing with uniforum's weird email templates. Disclaimer: I work at AWS.
79.
by mjb 2y ago
Look, a model checker! More seriously, it's interesting how this kind of thing is trivial to express in some languages (TLA+, prolog, Alloy), ok in some (Ruby, scheme), and super hard in others. The ruby model and specification would t
80.
by mjb 3y ago
Even more generally, distributed systems can find simpler solutions to things like "raise the throughput ceiling", and "handle disk failure", and "handle power failure" than single-box systems. This is for the
81.
by mjb 3y ago
The FIS and many other ski organizations are moving away from flouro wax: https://www.fis-ski.com/cross-country/news/2022-23/fis-to-fu...
82.
by mjb 3y ago
That's true too, this approach isn't limited to Reed-Solomon (or MDS codes). For non-MDS codes the fetch logic becomes a little more complicated (you need to wait for a subset you can reconstruct from rather than just the first k)
83.
by mjb 3y ago
It's true that Reed-Solomon isn't free. The first two codes (N of N+1 and N of N+2) are nearly trivial and can be done very fast indeed. On my hardware, the N of N+1 code (which is an XOR) can be arranged to be nearly as fast a me
84.
by mjb 3y ago
If folks are interested in more details about Lambda's container storage scheme, they can check out our ATC'23 paper here: https://www.usenix.org/conference/atc23/presentation/brooker
85.
by mjb 3y ago
Yeah, this is just trolling. There's nothing inherent to rust that requires ( or even recommends) writing code like this. There's nothing inherent to C that prevents bad API designs like this. Nothing about this post is notable or
86.
by mjb 3y ago
Yes, I think that's the most recent talk (and the most in-depth on this side of the problem).
87.
by mjb 3y ago
This is a cool series of posts, thanks for writing it! We've released a bit about how the AWS Lambda scheduler works (a distributed, but stateful, sticky load balancer). There are a couple of reasons why Lambda doesn't use this br
88.
by mjb 3y ago
However, in many real systems the aggregate behavior follows the asymptotic trend of the central limit theorem even though the underlying distributions may not fit the strict requirements.
89.
by mjb 3y ago
There's a whole area of math in "optimal stopping" which aims at exactly this question: how many dentists should you try before you pick your favorite? For example: https://en.wikipedia.org/wiki/Secretary
90.
by mjb 3y ago
The balls-into-bins problem comes up often in distribute systems engineering, and so it's super important to have the right intuition. I think a lot of people come in to the space assuming that random balls-into-bins is much more even

More ›