Metadata

My quest for a principled solution for metastable failures has taken me back to my roots on self-stabilization, as this recent paper related the problem to composition of self-stabilizing systems.  But, my literature search for recent work on composing self-stabilizing systems didn't yield anything useful. The layered stabilization idea was already in place by the early 2000s, and nothing fundamental seems to have been added since. Frustrating. So I decided to attack the problem using the concrete example I have. I had composed a rely-guarantee TLA+ model of a retry storm as two components with contracts . That model reproduces metastable failure because the composition that worked from good states failed to work when a large shock removes the base case that let the two conditions hold each other up. Searching for  rely-guarantee based composition from every state, turned up a 2017 control theory paper by Kim, Arcak and Seshia, "A Small Gain Theorem for Parametric Assume-Gua...

AI doomerism is everywhere these days. Every field, and recently humanity as a whole, has had its "we're finished" post. In contrast to the run-of-the-mill hot take, Jason Potts has written an economics paper on why academia is doomed . So let's dive in. What does a university sell? Potts says a university is really a platform. It is a hub that connects many different groups: undergrads, grads, teaching staff, research staff, employers, government, alumni, donors, parents, etc. Each group needs the others. Undergrad tuition helps pay for the research infrastructure for the professors whose research reputation drew the students there in the first place. International student fees provide funding for local students. Unfortunately, this isn't a diversified portfolio kind of situation, but more of a weakest-link setup. If you pull on one thread, several others start to come loose as well. ( Side remark : I will admit that I have always struggled to find the true custo...

Aleksey and I are back to reading papers live. This paper, Jetpack(OSDI '26), attempts building a universal 1-RTT fast-path framework that bolts onto existing leader-based consensus protocols with minimal modification. Why would we want this? Classic consensus protocols like Raft, Paxos, or Zab require two round-trip times (2 RTT) to commit a command: one RTT from client to leader, and another to replicate across followers. The extra RTT matters a lot for WAN deployments, so fast-path protocols (such as Fast Paxos, EPaxos, or SwiftPaxos) reduce this to 1 RTT by bypassing leader serialization, but unfortunately they tightly couple the fast path to the core protocol design. Production systems cannot easily swap out their battle-tested bespoke consensus engines, but if there was an add on that helped with latency especially in WAN deployments, that would be useful. The good news is that Jetpack is truly an add-on portable deal. It provides a shim layer that runs two execution paths i...

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

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