Metadata

Last week I wrote about modular verification of systems through open TLA+ specs and rely-guarantee discharge. In this post, I apply the same approach to study the metastability mechanics of a retry storm. Through this modeling I show that when the system is metastable, it is due to some trigger/shock that displaced the system outside the rely-guarantee discharge conditions of its components.  The model I use the retrier-server example from the "Characterizing Metastable Faults and Failures" paper and model it in TLA+ as a composition of a retrier and a server component. The shared interface between the two components consist of the following variables: qf : fresh work queued at the server qd : duplicate (retry) work queued at the server done : the count of fresh requests the server completed this round, which the retrier reads and clears turn : a flag forcing alternation between the retrier and server steps The retrier has one private variable, p , which denotes the pending...

Today, tech folk are scrambling to change their workflows to meet newly inflated 5X productivity quotas, while getting pummeled under the cognitive debt of agent-generated code. With every new model release, the gap is widening and humans are becoming more of a bottleneck in the loop, approaching closer to obsolescence as "coders". While the programmer's job description is getting completely refactored, writing remains surprisingly unaffected. LLMs have gotten very good at generating code, but I am appalled at the absolute shit they spew as prose. They always follow the same robotic cadence and cliches, and sprinkle the same tired vocabulary all around. They take my broken yet soulful writing and transform it into a plastic soulless word slop in the name of improving prose. Their writing communicates no actual understanding and insight. I think we are all developing a visceral ick reaction to AI writing. It is trapped in the uncanny valley, and it may be stuck there for ...

Preamble. This post came slowly, simmering over months really. So there is some stream of consciousness in here, and a lot of deliberating in public. The post is me learning modular verification and talking myself into it at the same time. Even pep-talking myself, because this is genuinely hard, and the field's standard advice is to avoid modular verification. But the advice is due for revision: LLMs plus TLAPS are quietly changing the economics that made monolithic spec the rational default. The compositionality problem TLA+ is compositional in the abstract sense... In the astral plane, a program execution is an infinite sequence of states, each state giving a value to every variable in an imagined universal state space. A spec is a predicate (yes/no test) on executions, which denotes a set of allowed executions. In this setup, the steps that change variables in other specs look like stuttering to yours. And that enables us to denote composition as a beautiful purely logical conj...

I am a distributed systems researcher. I mostly read and write about distributed systems and lightweight formal methods. But as my blog definition says, the blog is about "distributed systems broadly defined and other curiosities".  The last two years, LLMs were unavoidably the biggest part of those curiosities. However, I was still surprised how much I had written about them, when I went looking for a line I remembered coining. Something like, "LLMs are good at mediocrity, but really fast". I couldn't find the line, but instead I found a pile of my takes on LLMs scattered across the blog, and I figured it was worth collecting them into an index. So here it is, enjoy! I also threw in my overall take on LLMs that has stayed constant through their four years of reign so far.   Hot takes on LLMs Our Collective Bike Shed Moment (June 26) Are We Becoming Architects or Butlers to LLMs? (Feb 26) How LLMs may affect academic writing (Feb 26)  Agentic AI and The Mythi...

Specula is an agentic system that automates the process of software bug finding through authoring and model-checking a spec for the code. It derives TLA+ specifications automatically from the code, checks code-spec conformance through trace validation, model checks the spec to find concurrency bugs, and reproduces the bug at the code layer by writing integration tests with precise timing. I remember reading the Daikon paper "Quickly detecting relevant program invariants" in 2000 and getting impressed by it, and here we are after 26 years, solving the end-to-end problem much better than I ever thought would be possible in a push-button manner in the year of our lord 2026. But somehow, I am still somewhat unsatisfied with the paper. This may be me being hypercritical and trying to get more out of the paper by arguing with it . So bear with me until I resolve (or learn to accept) these problems over time. I know many of the authors of the Specula work, and respect them, and I...

This week, I presented this paper at ICCCN'26. This is joint work with Aleksey Charapko (University of New Hampshire) and my MongoDB colleagues Matt Broadstone, Daniel Gomez Ferro, and Akshat Vig. The paper investigates how to build a metastability tolerant execution control system (ECS) for a database. Why? Modern databases are complex networked systems serving mixed workloads: short queries (that want an answer in milliseconds) sitting next to analytics jobs (that want the CPU for multiple seconds). The arrival rate of requests is effectively unbounded, but of course, the server's resources are not. And, unfortunately, elastic scaling does not save you here. Scaling takes minutes, whereas, overload takes seconds. Admission control tries to guard the front door (more on this later), but the component that mediates contention once requests reach the backend is the execution control system (ECS). Unlike a closed system OS scheduler, which strives for fairness and completeness b...

The Aurora DSQL paper finally dropped . Reading it yesterday was an interesting experience, because I spent two years (2022-23) working with the AWS team that designed and built Aurora DSQL. Since I have been very familiar with the architecture, the paper's overview description of the system didn't excite me much. And if I am being honest, reading the paper also felt a bit dry, most likely because I am not doing the usual extra thinking to explore/understand the ideas in the paper. But taking a step back today, and leaving my subjective experience aside, I will try to elaborate on how the DSQL architecture is actually built on a set of aggressive and opinionated engineering bets.  If I had to explain this architecture in a single sentence (just as I used to do for other teams at AWS) it would be this: We took a traditional monolithic database and blew out every single component into an independent, horizontally scalable service. Exploding the Monolith DSQL divides the database ...

Metastability has been studied in previous work as a self-sustaining degradation in goodput that persists even after the trigger is gone. The degraded state loiters on entirely due to the system's own internal feedback loops (retries, queues), and there is no simple reset button to press in distributed systems. So this is not a rare exotic problem. Since production systems would have already been hardened to handle the obvious failures, what remains is these hard-to-detect emergent failures. The "Metastable Failures in the Wild" paper (OSDI'22) reports 22 incidents across 11 organizations. Four of the 15 major AWS outages in a decade were metastable failures, with durations ranging from 1.5 to 73 hours.  This paper (June 2026) argues that the systems community has treated metastability phenomenologically, which led people to chase symptoms rather than causes. The paper sets out to give the first analytical causal account of these failures. This framing leads to two...