Metadata

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 remem…

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 (th…

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…

Moving is not for the faint of heart! The surgeon general should issue a warning against moving houses after age 50 . Coordinating our cross-country move was one of the hardest thing I had done. Selling our house in Buffalo, finding a suitable rental house in the Bay Area, figuring out the logistics of the move, getting rid of the furniture we wouldn't transport, boxing everything up, and then on…

Looking at my peak male physique, and my Keanu Reeves baby face, you would never suspect it, but I recently turned 50. As is the tradition, I thought about writing a post titled "50 Lessons at 50". Unfortunately, I don't have that kind of wisdom. The thing is, I still feel like I'm 18, same age as my son. Turns out this is the secret old guys have been hiding from us all along. You get older only…

In 1957, Parkinson postulated his "Law of Triviality" using a fictitious committee reviewing plans for a nuclear power plant. The reactor design gets 10 minutes because nobody understands it, so nobody argues. The bike shed gets 45 minutes because everyone has opinions about the paint color. I feel like we are living this committee meeting at scale every day. LLMs are already better engineers tha…

We spent 10 days in Italy in early April. It was a lot of fun. Back when I was a grad student, I stayed in Pisa for a month for a "summer school on mobile computing" in 2003. Mobile computing was the next "big" thing back then. (In retrospect, the research was misguided about the local/distributed approach to it, as most of mobile computing reconciled to cloud backends as that is often more effic…

Shortly after I joined MongoDB research, we ran a TLA+ workshop. It was a two-day ordeal. We had a 1.5 days of instruction on TLA+ and syntax, after which we tried to help people get started with modeling. People liked learning about TLA+ on the first day, but except for a person or two, we didn't get anyone onboarded with TLA+ modeling. It was too much to offload on people and ask them to level …

The transformative power of LLMs in coding has been irrefutable, and it feels like we are living through a magical computing renaissance. On the socials, we hear impressive numbers of lines of code generated, features delivered, and bugs fixed. But, the macroeconomic indicators seem to be still lagging. Heck, if you talk with an engineering manager, you find that their product shipping dates have…

As I mentioned in my previous post , I traveled to San Jose at the end of May for the ACM CAIS conference. On Day 0, I gave a very short talk at the Supporting our AI Overlords (SAO) workshop. This post is the promised summary of our paper, "A Case for Simulation-Driven Resilience in Agentic Data Systems" , joint work with Aleksey Charapko (University of New Hampshire) and Akshat Vig (MongoDB). M…

Last week, I traveled to San Jose to attend the ACM CAIS conference . On Day 0, I gave a short talk at the Supporting our AI Overlords (SAO) workshop . And yes, I promise to write a summary of our paper, " A Case for Simulation-Driven Resilience in Agent-First Data Systems " soon! To start with an overall impression of the conference: much of the work presented felt exploratory and anecdotal. Sin…

Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate. It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white. You know what we do with concurrent systems here? Here we model them, and…

This is part of our series going through OSTEP book chapters. The OSTEP textbook is freely available at Remzi's website if you like to follow along. This chapter extends the CPU virtualization playbook to memory. It's the same recipe: let the program run directly on the hardware, but interpose at carefully chosen points so the OS retains control. For memory, this happens at every memory access. E…

I listened to this book as an audiobook through the Libby app, which basically brings your public library to your phone. The Thinking Machine is about Jensen Huang and the rise of Nvidia from graphics chips to AI dominance.  The author, Stephen Witt, is a long-form tech journalist. His writing is nice and clear. But it does not have a distinctive voice. I kept thinking of Michael Lewis , whose bo…

When talking about TLA+, I keep referring to "abstraction" as the most important thing to learn . And it is about the hardest to learn as well. But a contradiction has been bugging me. Aren't CS people already supposed to be good at abstraction? Isn't abstraction supposed to be at the root of OS, networking, software engineering? Abstract Data Types (ADTs) are a staple of every in CS curriculum. …

Ok, finally getting sometime to put my butt down to write about day 2 of BugBash. Why do so few buildings fall down? Brian Potter, Senior Infrastructure Fellow @ Institute for Progress, Author of Construction Physics  newsletter. Buildings rarely collapse. The rate of major structural failing is  between 1/100K to 1/ 1 million. (This is how I know this is a serious statistic: it is an interval.) …

These are my notes from the afternoon sessions of BugBash'26 . We had a 75 minute lunch break. Nice lunch, but there were no vegetarian entries, which made Peter Alvaro hangry. I don't blame him, I would be too. Informal methods Ben Eggers, Member of Technical Staff @ OpenAI This was a fun and also thought provoking talk. The premise is "Nothing has changed about software development". Really? Af…

Continuing with notes from the BugBash talks. Yes, all of this goodness, including Will Wilson's keynote was before lunch the first day. Where all the ladders start Peter Alvaro, Associate Professor of Computer Science @ UC Santa Cruz In this talk, Peter reflects back on his 20 years of distributing systems work. The cover image is Don Quixote (which is Peter)  attacking the windmill (robust dist…

I attended the BugBash 2026 these last two days, and had a blast. Here are my notes from the first keynote. I will try to find time to publish my notes from the other talks in the coming days. Keynote: We won, what now? Will Wilson, Co-founder & CEO @ Antithesis The Antithesis team opened with a great animation/teaser clip, then Will took the stage. Here is the summary of his talk. This is not a …