Posts

Showing posts from September, 2026

Metastability as a failed conditional discharge of rely-guarantee composition

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

Popular posts from this blog

The Safest Job from AI may be Writing

The Agentic Self: Parallels Between AI and Self-Improvement

Learning about distributed systems: where to start?

Hints for Distributed Systems Design

Building a Database on S3

Foundational distributed systems papers

Cloudspecs: Cloud Hardware Evolution Through the Looking Glass

Specula: Scaling formal specifications for autonomous model checking of system code

What I'd do as a College Freshman in 2025

Aurora DSQL: Scalable, Multi-Region OLTP