Posts

Showing posts from April, 2025

Multi-Grained Specifications for Distributed System Model Checking and Verification

Image
This EuroSys 2025 paper wrestles with the messy interface between formal specification and implementation reality in distributed systems. The case study is ZooKeeper. The trouble with verifying something big like ZooKeeper is that the spec and the code don’t match. Spec wants to be succinct and abstract; code has to be performant and dirty.  For instance, a spec might say, “this happens atomically.” But the actual system says, “yeah, buddy, right.” Take the case of FollowerProcessNEWLEADER: the spec bundles updating the epoch and accepting the leader’s history into a single atomic step. But in the real system, those steps are split across threads and separated by queuing, I/O, and asynchronous execution. Modeling them as atomic would miss real, observable intermediate states, and real bugs. To bridge this model-code gap, the authors use modularization and targeted abstraction. Don’t write one spec, write multi-grained specs. Different parts of the system are modeled at different ...

What I'd do as a College Freshman in 2025

Do Computer Science Absolutely. Still would. Many are spooked by LLMs. Some, like Jensen Huang, argue that "nobody has to learn how to program."   I argue the opposite . And I double down.  Being supported by AI tools is not a substitute for mastery . You can’t borrow skills. You have to earn them.   Computer science builds vital skills : hacking, debugging, abstract thinking, and quick adaptation. These don’t go out of style.   Do STEM. It’s LLM-resistant. LLMs can retrieve and remix information, but do you know what to do with them? Like the dog chasing the car, what now? STEM teaches you that. It teaches you to think, to reason, to act. It gets you from information to wisdom. But only after you've mastered the foundations. We're heading into the age of Ï€-shaped people: depth in two areas, and generalist across . Building depth first, and then ranging is good strategy .   So yes, I would learn the foundations of both CS and AI. And then do AI + X, where X is s...

Popular posts from this blog

Hints for Distributed Systems Design

My Time at MIT

Making database systems usable

Advice to the young

Looming Liability Machines (LLMs)

Learning about distributed systems: where to start?

Foundational distributed systems papers

Scalable OLTP in the Cloud: What’s the BIG DEAL?

Distributed Transactions at Scale in Amazon DynamoDB

Linearizability: A Correctness Condition for Concurrent Objects