Marc Brooker

Databases, serverless, and serverless databases at AWS. Interested in distributed systems, databases, operating systems, virtualization, and remote sensing. I read a lot of papers.

Check out my blog at https://brooker.co.za/blog/

Views are my own.

Blog: https://brooker.co.za/blog/
GitHub: https://github.com/mbrooker

Public Key

npub1tmlvx33fj5fykqfvupx76fxprlrew9jjgu7cvk04puxscgzgfv8ss5tztd

NIP-05 Address

[email protected]

Profile Code

nprofile1qqs9alkrgc5e2yjtqykwqn0dynq3l3uhzefyw0vxt86s7rgvypyykrcprpmhxue69uhhyetvv9ujumt0d4hhxarj9ecxjmntnv9kjt

Publishing to

relay.momostr.pink

Author Public Key

npub1tmlvx33fj5fykqfvupx76fxprlrew9jjgu7cvk04puxscgzgfv8ss5tztd

Show more details

Last Notes

2025-07-14 23:20:20 GMT

I sat down with Darko Mesaros to talk about Kiro, specification-driven development, and putting AI-powered development in context of the history of computing.
Is an LLM a compiler? What is a spec? How are specs like SQL? Check it out:
https://www.youtube.com/watch?v=OdD9eLiRRVo
and be sure to check out https://kiro.dev/

2025-06-02 16:42:21 GMT

New blog post, about some of my favorite papers from this year's HotOS program. Love Little's law? Hate fork? Think static analysis of shell programs sounds fun? Had enough of the f threshold model? Check it out for some papers to read: https://brooker.co.za/blog/2025/06/02/hotos.html

2025-05-07 16:47:17 GMT

- reply

Thanks for pointing this out. We'll get it fixed.

2025-05-03 16:50:16 GMT

- reply

As far as I know, this issue has existed in PostgreSQL since the introduction of MVCC more than two decades ago. It affects most clustered installations of PostgreSQL. We are working with the PostgreSQL community on a fix.
This issue doesn't affect Amazon Aurora Limitless Database, or Aurora DSQL. Both of these databases use different methods for ordering transactions, which provide a consistent ordering across replicas.

2025-05-03 16:49:54 GMT

Recently, one of our testing tools at AWS found an issue with transaction visibility in PostgreSQL, where the order that transactions become visible differs between the primary and replicas. Sergey Melnik dives deep on the AWS Database Blog: https://aws.amazon.com/blogs/database/understanding-transaction-visibility-in-postgresql-clusters-with-read-replicas/

2025-04-28 17:05:09 GMT

- reply

But that "do what Postgres does" doesn't extend to the distributed features, and is insufficiently precise for some kinds of correctness. TLA+ and P fit in well there.

2025-04-28 17:04:17 GMT

- reply

TLA+ as a correctness oracle for deterministic (or even non-deterministic) simulation testing makes a ton of sense to me.
As you say, a big part of that is driving folks to think about what correctness means to them.
In DSQL testing, for example, we've used "do what Postgres does" as a correctness oracle for a lot of the non-distributed surface area, just because that's what many of our customers care about.

2025-04-26 16:57:12 GMT

- reply

Yes, I agree. I'm (obviously) a big TLA+ fan, but it is increasingly difficult to see where it's going to fit into our practice broadly. Very likely to continue to remain popular as a niche tool (for good reasons), and maybe that's enough.
The connection between TLA+ and deterministic simulation is a very interesting one. At some level, they have very similar mental models.

2024-12-11 17:03:03 GMT

- reply

100s for a single primary key, although we'll improve that over time.

2024-12-06 17:26:15 GMT

The fourth and last in my series of blog posts on our new Aurora DSQL database is up! This time, we're looking at what happens during network partitions, and how we preserve consistency, availability, and durability. Check it out: https://brooker.co.za/blog/2024/12/06/inside-dsql-cap.html
https://fediscience.org/system/media_attachments/files/113/607/047/365/921/762/original/371a54cf4f26aebe.jpg

2024-12-05 18:08:55 GMT

Today's third blog post on Aurora DSQL: this time looking at the write and commit path, and how conflicts are detected and handled: https://brooker.co.za/blog/2024/12/05/inside-dsql-writes.html

2024-12-04 17:11:17 GMT

My second blog post on Aurora DSQL, with a deep dive on how reads work: https://brooker.co.za/blog/2024/12/04/inside-dsql.html

2024-11-21 00:06:11 GMT

Rust Foundation Collaborates With AWS Initiative to Verify Rust Standard Libraries https://foundation.rust-lang.org/news/rust-foundation-collaborates-with-aws-initiative-to-verify-rust-standard-libraries/
Verify the Safety of the Rust Standard Library https://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/

2024-11-14 17:26:38 GMT

New blog post on ten years of AWS Lambda, and some thoughts on the Lambda PRFAQ: https://brooker.co.za/blog/2024/11/14/lambda-ten-years.html

2024-11-01 22:39:30 GMT

I'm on the AWS Developers podcast this morning, talking to Julian Wood about AWS Lambda's 10th anniversary, the growth of serverless, and some of what we learned along the way.
https://developers.podcast.go-aws.com/web/podcasts/episode_137/index.html

2024-10-22 15:30:03 GMT

- reply

Most of this is using formal logic to reason about mathematical specifications of systems. But LLMs are useful in this space too - for example I find them super useful for brainstorming proof strategies (how do I proof this), and accelerating formal model development. Semantic search is also super helpful.
There's a bright future in combining these techniques. They tend to be good at complementary things.

2024-10-21 15:53:52 GMT

- reply

"But what about time-to-market?" has been one of the objections to automated reasoning and formal methods forever, but in many domains they allow us to get to market faster. This is especially true in security, availability, and durability-critical domains.

2024-10-21 15:53:32 GMT

Great new piece from Byron Cook about automated reasoning at AWS, and how we're finding it not only allows us to deliver safer code, but also deliver faster code, and deliver code faster. https://aws.amazon.com/blogs/security/an-unexpected-discovery-automated-reasoning-often-makes-systems-more-efficient-and-easier-to-maintain/

2024-08-14 19:20:46 GMT

New little blog post on garbage collection and metastability: https://brooker.co.za/blog/2024/08/14/gc-metastable.html

2024-08-08 15:05:07 GMT

More great work from Kyle, and another reminder that retrying isn't the safe best-practice that many folks assume it is: https://jepsen.io/analyses/jetcd-0.8.2

2024-08-07 23:43:16 GMT

- reply

The tool I use most often is P, with a bit of TLA+, Kani, and (lately) Lean. I've also been learning more about Dafny, but I (personally) haven't done anything real with it yet.

2024-08-07 19:48:25 GMT

- reply

I've been learning Lean recently to add to my formal toolkit, and it's been a really eye-opening experience. I don't have much of a math background, but have already found Lean lets me do things that I found really hard before.
https://fediscience.org/system/media_attachments/files/112/922/466/896/012/670/original/b2a2bf13d5ba76a5.png

2024-08-07 19:47:44 GMT

Loved this talk by Terence Tao on math, AI, and proof assistants. I suspect we're going to see a similar effect in software: AI will allow formal specs to be developed faster than traditional programs, and for programs to be generated from those specs. https://www.youtube.com/watch?v=_sTDSO74D8Q
https://fediscience.org/system/media_attachments/files/112/922/460/279/079/365/original/2adc211215e17f38.png

2024-06-04 21:47:05 GMT

New blog post, on the "you don't need distributed systems" meme, and the idea that distributed systems are only about scale: https://brooker.co.za/blog/2024/06/04/scale.html
Short version: scale is only a tiny part of what makes distributed systems interesting and useful.

2023-07-02 16:01:13 GMT

- reply

And don't forget the jitter! https://aws.amazon.com/builders-library/timeouts-retries-and-backoff-with-jitter/

2023-07-02 16:00:55 GMT

- reply

Exponential backoff. Like quotas, backoff works well in systems with a bounded number of clients ("closed systems"), where clients actually back off. In systems with more new customers coming in all the time, backing off just delays work, and doesn't reduce it.
Delaying work increases time-to-recovery after overload. See more at: https://brooker.co.za/blog/2022/08/11/backoff.html

2023-07-02 16:00:14 GMT

- reply

Quotas. Quotas work well in systems with a well-bounded number of clients, and where those clients correctly respect the "quota exceeded" response. If either of these things aren't true - even in the case of bad actors - they don't tend to work.
Do social media networks have a bounded number of clients? At first glance they're an "open" system, with large numbers of clients. I suspect a lot of load comes from a small number of heavy hitters. See more on open vs closed: https://brooker.co.za/blog/2023/05/10/open-closed.html

2023-07-02 15:59:08 GMT

The internet is talking about retries and backoff! As we've seen over the last day or so, simply retrying without backoff leads to an unbounded increase in work. This, in turn, tends to make overloaded systems even more overloaded. What can we do instead?