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

Last Notes

2025-05-03 16:50:16 UTC

- 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 UTC

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:04:17 UTC

- 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.

2024-12-11 17:03:03 UTC

- reply

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

2024-12-04 17:11:17 UTC

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 UTC

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-10-21 15:53:32 UTC

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-08 15:05:07 UTC

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 UTC

- 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 UTC

- 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 UTC

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 UTC

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 15:59:08 UTC

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?