Posts

Showing posts from May, 2026

Chess invariants

Image
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 we distill their invariants. Here is some setup definitions first. In a CS or math paper, if you write "Section 2: Model and Problem" well enough, the rest of the paper writes itself. With this setup you can sort of see what the actions will be. In fact, forget about the actions. Let's look at some invariants. Invariants When deriving invariants we ask: what must always be true? I find it useful to split the safety invariants into two camps: state invariants (which are predicates over a single state) and transition invariants (which are predicates over a step). The transition inv...

OSTEP Chapter 15: Address Translation

Image
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. Every load, store, and instruction fetch gets translated by hardware from a virtual to a physical address. The mechanism here is called dynamic relocation , dating to the late 1950s. The base register holds the physical address where the process's address space starts, the bounds register holds its size. On every memory reference the hardware adds base and checks against bounds. If the address is out of range, the CPU raises an exception, and the OS kills the offender. This takes collaboration between hardware and the OS. Hardware provides privileged mode, the base/bounds registers...

Book review: The Thinking Machine

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 books have more narrative personality and rhythm. The book is written for a lay audience. Technical ideas are explained in simplified terms. Much of these were already familiar to me, and I had also lived through Nvidia going from graphics cards to AI chips. (I wish I had bought more stock.) I was hoping to learn more about Jensen, his philosophy, habits, inner life, management style. There is not much of that in the book. I think that absence is telling. Jensen comes across as a very private person, and almost monastic about work. There does not seem to be a boundary there: he has become one...

The Two Abstractions of System Design: Hide or Reduce

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. So why do I (and every other formal methods/modeling person) see such a large skill gap in abstraction, and flag it as the core, make-or-break skill for modeling? I think I finally get to the root of this cognitive disonance. There are two kinds of "abstraction" conflated under the same umbrella term. Modularity abstraction: This is the traditional abstraction taught in CS curricula as ADTs, APIs, layered design, etc. It is all about encapsulation, drawing boundaries, and hiding internals. Modeling abstraction: This is what I talk about when I talk about abstracti...

BugBash'26: Day 2

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.)  Why don't more buildings fall down? There are some technical reasons to it: buildings are simple stuctures with no (or little) moving parts. Buildings exhibit a limited number of behavior when you load their structure: stress, deflection, vibration, creep, etc. And these behaviors are commensurate to the  proportion of the force you put in. Finally, buildings are designed for 2X-3X of expected load. Let's go deeper into structural elements. We have good theories for how structural elements behave, and individual components are tested extensively and are standardized. A build...

Popular posts from this blog

Hints for Distributed Systems Design

Chess invariants

The Agentic Self: Parallels Between AI and Self-Improvement

Learning about distributed systems: where to start?

Foundational distributed systems papers

Building a Database on S3

Cloudspecs: Cloud Hardware Evolution Through the Looking Glass

TLA+ mental models

Advice to the young

Analyzing Metastable Failures in Distributed Systems