Metadata

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 …

This is a short chapter covering the nuts and bolts of memory allocation in C: malloc(), free(), and the many ways programmers get them wrong. 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. Stack vs. Heap C gives you two kinds of memory. Stack memory is automatic: the compiler allocates it when y…

Paxos consensus protocol, despite its many theoretical virtues, is fundamentally rude. One need only look at the way it behaves to see the problem. A leader seizes power. It dictates values. When two leaders happen to propose simultaneously, they do not pause, tip their hats, and work things out over tea. No,  they duel, each furiously incrementing ballot numbers at the other like barbarians enga…

This paper from METR (Model Evaluation & Threat Research) introduces a new metric for tracking AI progress: the "50%-task-completion time horizon". This denotes the length of software engineering task (measured by how long a skilled human developer takes to complete it) that the AI model can finish with 50% success rate. The researchers evaluated 12 frontier AI models on 170 tasks across three be…

Chapter 13 of OSTEP provides a primer on how and why modern operating systems abstract physical hardware. 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. Multiprogramming and Time Sharing In the early days of computing, machines didn't provide much of a memory abstraction to users. The operating s…

This paper presents SysMoBench, a benchmark designed to evaluate generative AI's ability to formally model complex concurrent and distributed systems. Although the paper is published on January 2026, the AI landscape moves so fast that the models evaluated (like Claude-Sonnet-4 and GPT-5) already feel dated, after the release of heavy hitters like Claude 3.5 Opus or OpenAI's Codex. The paper draw…

In the age of LLMs, syntax is no longer the bottleneck for writing, reading, or learning TLA+. People are even getting value by generating TLA+ models and counterexamples directly from Google Docs descriptions of the algorithms. The accidental complexity of TLA+ (its syntax and tooling) is going away. But the intrinsic complexity remains: knowing where to start a model, what to ignore, and how to…

As I mentioned in my previous blog post, I recently got my hands on Claude Code. In the morning, I used it to build a Hybrid Logical Clocks (HLC) visualizer . That evening, I couldn't pull myself away and decided to model something more ambitious. I prompted Claude Code to design a Paxos tutorial game, BeatPaxos, where the player tries to "beat" the Paxos algorithm by killing one node at a time a…

Yesterday morning I downloaded Claude Code, and wanted to see what this bad boy can do. What better way to learn how this works than coding up a toy example with it. The first thing that occurred to me was to build a visualizer for Hybrid Logical Clocks (HLC). HLC is a simple idea we proposed in 2014 : combine physical time with a logical counter to get timestamps that are close to real time but …

This chapter from Operating Systems: Three Easy Pieces explores multiprocessor scheduling as we transition from the simpler world of single-CPU systems to the challenges of modern multicore architectures. 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. Core Challenges in Multiprocessor Scheduling …

When you are in TPOT echo chamber, you would think fully autonomous AI agents are running the world. But t his 2025 December paper, "Measuring Agents in Production", cuts through the reality behind the hype. It surveys 306 practitioners and conducts 20 in-depth case studies across 26 domains to document what is actually running in live environments. The reality is far more basic, constrained, and…

Retry storms are infamous in distributed systems. It is easy to run into them. Inevitably, a downstream service experiences a hiccup, so your clients automatically retry their failed requests. Those retries add more load to the struggling service, causing more failures, which trigger more retries. Before you know it, the tiny unavailability cascades into a full-blown self-inflicted denial of serv…

This paper proposes a way to get serializability without completely destroying your system's performance. I quite like the paper, as it flips the script on how we think about database isolation levels. The Idea In modern hardware setups (where we have massive multi-core processors, huge main memory, and I/O is no longer the main bottleneck), strict concurrency control schemes like Two-Phase Locki…