Hey Will. I'm a huge fan of the work you all are doing, and of FoundationDB, but I don't believe it's accurate that DST was invented at FoundationDB (or, maybe it was, but was also used in other places around the same time or before).
For example, the first implementations of AWS's internal lock service (Alf) used DST as a key part of the testing strategy, sometime around 2009. Al Vermeulen was influential in introducing it at AWS, and I believe it built on some things he'd worked on before.
Still, Anithesis is super cool, and I really admire how you all are changing the conversation around systems correctness. So this is a minor point.
Also a huge proponent of Antithesis and their current work, but there definitely were some notable precedents at or around that time e.g. MODIST from 2009 (https://www.usenix.org/legacy/event/nsdi09/tech/full_papers/...), which similarly tried to build a "model checker for distributed systems".
As another interesting historical side note, I have wondered about the similarities between Antithesis and "Corensic", a startup spun out of UW around a similar time period (circa 2009). Apparently, they "built a hypervisor that could on-demand turn a guest operating system into deterministic mode" (see "Deterministic Multiprocessing" at
https://homes.cs.washington.edu/~oskin/). My impression is that their product was not a significant commercial success, and the company was acquired by F5 Networks in 2012 (https://comotion.uw.edu/startups/corensic/).
Overall, I don't over-index on novelty, and think it is generally good for ideas to be recycled/revived/re-explored, with updated, modern perspectives. I believe that most rigorous systems designers/engineers likely converge to similar ideas (model checking, value of determinism, etc.) after dealing with these types of complex systems for long enough. But, it is nevertheless interesting to trace the historical developments.
Corensic was impressive tech. I actually debriefed with one of their founders years ago. IIRC, their product was focused on finding single-process concurrency bugs.
Deterministic hypervisors are by no means new. Somebody once told me that VMWare used to support a deterministic emulation mode (mostly used for internal debugging). Apparently they lost the capability some time ago.
Hi Marc, thank you for the correction! We started doing it around 2010, and were not aware of any prior art. But I am not surprised to hear that others had the idea before us. I will give Al credit in the future.
I (one of the authors) did some distributed systems work with Promela about a decade ago, but it never felt like the right fit in the domain. It's got some cool ideas, and may be worth revisiting at some point.
> Maybe one can transform slow code from high level languages to low level language via LLMs in future.
This is one of the areas I'm most excited for LLM developer tooling. Choosing a language, database, or framework is a really expensive up-front decision for a lot of teams, made when they have the least information about what they're building, and very expensive to take back.
If LLM-powered tools could take 10-100x off the cost of these migrations, it would significantly reduce the risk of early decisions, and make it a ton easier to make software more reliable and cheaper to run.
It's very believable to me that, even with today's model capabilities, that 10-100x is achievable.
I remember many years back one of Go language author wrote C to Go trasformer and used that to convert all compiler, runtime, GC etc into Go.
Now in today's time some experts like above could create base transformer for high level language and frameworks to low level language and frameworks and this all get exposed via llm interfaces.
One can say why all this instead of generating fast binary directly from high level code. But generating textual transformation would give developers opportunity to understand, tweak and adjust transformed code which generating direct binary would not.
Which features would you like to see the team build first? Which limits would you like to see lifted first?
Most of the limitations you can see in the documentation are things we haven't gotten to building yet, and it's super helpful to know what folks need so we can prioritize the backlog.
indexes! vector, trigram and maybe geospatial. (some may be in by now I didn't follow the service as closely as others)
note, doesn't have to be pg_vector pg_trgm or PostGIS, just the index component even if it's a clean room implementation would make this way more useful.
My understanding is the way Aurora DSQL distributes data widely makes bulk writes extremely slow/expensive. So no COPY, INSERT with >3k rows, TRUNCATE etc
This makes sense, especially with the move of OSDI to being annual, and NSDI accepting more and more general systems-y work (e.g. we published the Firecracker paper at NSDI, which wouldn't have made sense even 5 years earlier). ATC was left in a difficult niche, but still a valuable venue for "hackier" systems work, industry systems papers of the less quantitative kind, and a few others.
I'd love to see OSDI evolve to accept more of this work, and look at the ATC work that has stood the test of time and accept more work like that. Maybe SOSP and Eurosys too. I bet USENIX is going to figure this out - they're generally a smart and well-run organization.
Fun fact: we won best industry paper at ATC'23 for "On-demand container loading in AWS Lambda" (https://www.usenix.org/conference/atc23/presentation/brooker). I was super happy with it as a paper and got a ton of good feedback on it. About six months earlier, it'd been desk-rejected by the chair of another systems conference who asked that we don't submit such low-quality work to them.
This is great, really worth reading if you're interested in transactions.
I liked it so much I wrote up how the model applies to Amazon Aurora DSQL at https://brooker.co.za/blog/2025/04/17/decomposing.html It's interesting because of DSQL's distributed nature, and the decoupling between durability and application to storage in our architecture.
DSQL is so cool - have been following since the release and once it supports more of the postgres feature set + extensions it’ll be a killer. Fantastic architecture deep dive at ReInvent as well.
MySQL Serializable is pretty similar to serializable in other databases, in terms of the observable anomalies. There's a good set of tests here: https://github.com/ept/hermitage
> So maybe I'm supposed to consider this post only for 'Every transactional system' running with SERIALIZABLE transaction isolation.
No, it's a general point about the nature of transactions in DBMSs, and the different implementation choices. As the article says, there are some variations (e.g. MVCC at levels lower than serializable inherently has two 'order' steps).
I'm not seeing the mention of two 'order' steps. Are you referring to the larger part of what I quoted?
> MVCC databases may assign two versions: an initial read version, and a final commit version. In this case, we’re mainly focused on the specific point at which the commit version is chosen — the time at which the database claims all reads and writes occurred atomically.
For non-SERIALIZABLE isolation there may be no such "time at which the database claims all reads and writes occurred atomically", which is how I took the rest of the post to mean when running with SERIALIZABLE isolation.
It is written with a lean towards serializable, partly because there's a wide variety of easy examples to pull which all implement serializable, but the ideas mostly extend to non-serializable as well. Non-serializable but still MVCC will also place all of their writes as having happened at a single commit timestamp, they just don't try to serialize the reads there, and that's fine. When looking at non-serializable not MVCC databases, it's still useful to just try to answer how the system does each of the four parts in isolation. Maybe I should have been more direct that you're welcome to bend/break the mental model in whatever ways are helpful to understand some database.
The line specifically about MySQL running at serializable was because it was in the Spanner section, and Spanner is a (strictly) serializable database.
Thanks for the clarifications and diagrams. I can see how using something like Spanner from the outset makes sense to use and stick with serializable isolation. With other SQL dbs, I've mostly seen repeatable read, read committed, and even read uncommitted used in the name of performance. Read committed works fine but you have to design everything for it from the start with thoughtful write and read sequences.
Moving to serializable should be easy but isn't in the case of Spanner and the like because you can't make 100+ of sub-millisecond queries to respond to an API request if that's how your app evolved.
The way I imagine the future is to bring the code closer to the data like stored procedures, but maybe in a new way like modern languages compiled to run (and if necessary retry) in a shard of the database.
I'll guarantee my UHC 1080 cleaver will slam a good distance through your stainless steel knife edge-on. Your chosen steel has toughness but it lacks in actual strength.
Strength very rarely matters in knife blades, unless you use knives as pry bars (strength determines the force required to either break the blade or cause a permanent plastic deformation of the blade, i.e. to permanently bend the blade).
What matters is the compromise between hardness (good for edge retention) and toughness (required to avoid chipping).
Many alloyed steels (especially with chromium and vanadium) allow a better compromise than simple carbon steels, i.e. either a higher toughness at equal hardness or a higher hardness at equal toughness.
When you do not specify simultaneously hardness and toughness, simple carbon steels may seem good enough, because they can be made to be either very hard or very tough.
If you cut only very soft things, like fish meat without bones, a very hard carbon steel blade (like a traditional Japanese yanagiba) will not have any disadvantage versus an alloyed steel blade. When you want a more versatile knife, an alloyed steel blade will be superior.
Another thought this triggered for me, related to photo:
A lot of hobbies as they digitize have moved to having 0 OpEx but much higher CapEx.
Photography for example, bodies/lenses didn't change much for 10-20 years, and didn't cost that much. There was recurring expense for film/dev/prints that scaled with your usage, and arguably you could GAS out on those smaller purchases.
In the film era for reference, you had Nikon F 1959, F2 1971, F3 1980, F4 1988, F5 1996, F6 2004. The entire film era Nikon had 6 flagships in 45 years! You could use the same camera for 20 years and only be maybe 1~2 generations behind at the end! There just wasn't much to upgrade to.
With digital bodies cost a ton, and even as we've slowed advancement.. you still get a new flagship body every 3-4 years (down from as little as 2 years in the early Sony A7 days). Some is tech advancement but a lot of it is parcelling out improvements sparingly cycle by cycle to try to drive sales in our modern higher consumption era.
For example, the first implementations of AWS's internal lock service (Alf) used DST as a key part of the testing strategy, sometime around 2009. Al Vermeulen was influential in introducing it at AWS, and I believe it built on some things he'd worked on before.
Still, Anithesis is super cool, and I really admire how you all are changing the conversation around systems correctness. So this is a minor point.
reply