In Search of a Compositional Theory of Self-Stabilization

A September 21, 2026 post on the Metadata blog asks whether self-stabilization admits a compositional theory. The author's search for a principled account of metastable failures led him back to self-stabilization, and a sweep of the literature on composing such systems found nothing useful. His test case is a rely-guarantee TLA+ model of a retry storm built from two components with contracts, which reproduces a metastable failure when a shock removes the base case holding the two conditions up.

From one promise to a family of contracts

Searching for rely-guarantee composition from every state turned up a 2017 control theory paper by Kim, Arcak and Seshia. It discharges circular reasoning between two components, but a component is a memoryless input-output relation on signals: backlog cannot be expressed, queues are out of reach, and stabilization is not addressed.

The core idea is still worth borrowing. Instead of one preconditioned promise — “if the queue is under 6, I send no retries” — it writes a family of contracts for every case: whatever the queue length L, the component sends at most λ(L) retries, and the table runs from “queue at most 6 → 0 retries” to “queue at most 18 → 6 retries”.

Why the small gain shortcut fails

The small gain theorem says a loop settles when its component gains multiply to less than one. Two things block it here: it needs straight lines, but only the retrier has a fixed slope of 1/2 while the server's share goes as f/(f+d); and it assumes badness is one number, while there are two queues: fresh work and duplicates.

Tracking both gives a fixed point at (8,4) and four slopes. The diagonal entries, 11/12 and 5/6, are memory — the share of each queue still present next round. The off-diagonal ones, 7/12 and 1/6, are coupling between the queues. Multiplying only the coupling gives 7/72 ≈ 0.1, which reads as stable with tenfold margin — and is wrong, because it ignores memory. The full linear stability analysis gives 1.19 and 0.56: one above one, so almost any disturbance grows.

Known fixes, and a ceiling that does not help

The arithmetic explains the fixes in use. A retry budget zeroes the 7/12 entry; fresh-first service zeroes the 1/6. Either way the factors return to 0.92 and 0.83, and backlog drains 8% per round instead of growing 19%. Capping queues is the same move: a cap M limits the retrier to (M−6)/T retries — M=7 allows none and every start drains, M=8 allows one and other attractors appear. At M=40 the system parks at (39,38): of three units served per round, one does useful work and two feed duplicates already in flight — metastability by definition.

The upshot is partial. The paper gave a better way to state a promise as a family of contracts, but no composition recipe, and its memoryless, scalar model does not fit the example. The four slopes came from writing out both queues together, abandoning composition for that step. Still, every term belongs to one component: 7/12 is the retrier's 1/2 plus the server's 1/12.