In Search of a Compositional Theory of Self-Stabilization

My literature search for recent work on composing self-stabilizing systems didn't yield anything useful. The layered stabilization idea was already in place by the early 2000s, and nothing fundamental seems to have been added since. Frustrating.

So I decided to attack the problem using the concrete example I have. I had composed a rely-guarantee TLA+ model of a retry storm as two components with contracts. That model reproduces metastable failure because the composition that worked from good states failed to work when a large shock removes the base case that let the two conditions hold each other up.

Searching for  rely-guarantee based composition from every state, turned up a 2017 control theory paper by Kim, Arcak and Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts". This paper does roughly what I want: discharging circular reasoning between two components without layering or blocking. But it comes with some serious limitations. In their formalism, a component is an input-output relation on signals, and contracts relate an input bound to an output bound. This is a memoryless view of a component, so it is not possible to express backlog accumulating from previous rounds. That rules out queues, among other useful distributed systems concepts. It also has no connection to stabilization. The paper does not talk about a variant/potential function and convergence reasoning. But there are still pieces there worth stealing toward a compositional theory of self-stabilization and metastability. Below I try to work this out... somewhat unsuccessfully.

Understanding Parametric Assume-Guarantee Contracts

In our original model, the retrier's guarantee was conditional and partial: "if the queue is under 6, I send no retries". This contract does not say anything about when the queue is at 18. Since the "if" condition fails, the promise is vacuously satisfied and the component owes us nothing.

The parametric assume-guarantee paper's big idea is to write a whole family of contracts that cover everywhere, rather than writing one promise with a precondition.

Tired: If the queue is under 6, no retries.

Wired: Whatever the queue length $L$ turns out to be, I send at most $\lambda(L)$ retries.

Recall that my constants from the model are $S=3$ units of server capacity per round, $A_{max}=2$ maximum fresh arrivals per round, and a retry timeout of $T=2$ rounds, which makes the latency threshold $S \cdot T = 6$. This makes $\lambda(L) = \lfloor (L-6)/2 \rfloor$, which gives us:

if the queue is at most...	...I send at most this many retries
6	0
8	1
10	2
12	3
14	4
16	5
18	6

The old contract is still in there, as the top row: $\lambda(6)=0$ says "queue under 6 means at most zero retries". Although the old contract is invalid at queue length of 18, under the parametrized assume-guarantee approach every row of the table gets a promise. So we get a bundle of ordinary contracts, one per badness level $p$:

$$\varphi_a = \bigvee_p \psi_a(p)$$

$$\varphi_g = \bigwedge_p \left( \psi_a(p) \Rightarrow \psi_g(\lambda(p)) \right)$$

The assumption side, $\varphi_a$, is a disjunction because the levels are alternatives. The environment will be at one of them, whichever one it happens to be. "Queue at most 6, or at most 8, or at most 10, or..." is satisfied by essentially any environment, so there is no envelope left to fall outside of.

The guarantee side, $\varphi_g$, is a conjunction over the same levels. Since the obligations are cumulative, we owe all of them at once. Rows whose condition is false cost us nothing, and since the levels are nested, several apply at once and the tightest wins. When queue is at 7, "at most 8" applies, and the component owes us at most 1 retry; "at most 10" also applies and it also owes us at most 2, but the first case already implies that. Monotonicity becomes key here.

Deriving the Small Gain Rule

What is the rule that says when such a loop settles? The paper calls this the small gain theorem. Let me start by explaining the intuition.

You have seen this happen, right? When a microphone gets in front of a speaker, the mic picks up sound, and the amp boosts it. The speaker plays this back, which the mic picks it up again. Each lap around that loop multiplies the sound, and you hear a high pitched squeal.

To quantify this process we need one number per component: how much badness out per unit of badness in. That is the slope of the component's response function, and control theory calls it the component's gain.

When we chain the two components, and feed a nudge $x$ into the first, slope $g_1$, and $g_1 x$ comes out. When we feed that into the second, slope $g_2$, and $g_2 g_1 x$ comes out. One lap has multiplied the nudge by $g_1 g_2$. After $k$ laps the nudge is $(g_1 g_2)^k$ times its original size. If the product is under one, the laps shrink geometrically and the loop settles. If it is over one, it diverges. The proof is from the geometric series.

The small gain theorem is so elegant, it gives us a global result that covers every starting state at once. But the small gain setup is limited. In our case, two things stop us from using this shortcut.

First, this needs straight lines. Our retrier has a straight slope $1/2$, but our server does not. Its share of service goes as $f/(f+d)$, so its slope depends on where the queues are. So, there is no single number to multiply.

Second, and worse, the shortcut assumes badness is one number. Our system has two queues that behave differently: fresh work $q_f$, and duplicates $q_d$. A bound on one is not a bound on the other. So a lap around our loop takes a pair of numbers to a pair of numbers.

Underneath both limitations lies the memoryless view of a component I complained about in the introduction. In this setup a gain is an input-output relation: it says how much of what arrives is passed along. There is no slot in it for how much of my own backlog is still sitting here from previous rounds. Queues are mostly backlog, and that is what the next section is about.

Dealing with Two Queues and Four Slopes

Let's track both queues. We can write the round as a rule on the pair (fresh queue $f$, duplicate queue $d$) by applying arrivals, applying retries, applying the proportional service split to figure out the next pair. We then ask whether any pair maps to itself.

One pair does: $(f,d) = (8,4)$. Here the total queue is 12, so the three units of capacity split two to fresh and one to duplicates. Two fresh served cancels the two arrivals exactly. The retry rate is $(8-6)/2 = 1$, and one duplicate served cancels that exactly. So next rounds, the queues are still in balance.

The question is what happens if we start near this balance point. Start at $(9,4)$ and does the system fall back, or run away? To answer we need to know how a small nudge propagates.

I will save you the calculation but here is the table.

	effect on next \(f\)	effect on next \(d\)
per unit of \(f\)	\(11/12\)	\(7/12\)
per unit of \(d\)	\(1/6\)	\(5/6\)

Let's start with the diagonal. Here we reason about what happens if we add one item to a queue, how much bigger does that queue get next round? For this reasoning, only the server is involved, and we get $11/12$ and $5/6$, which are the fraction of that item still sitting there next round.

Now, let's consider the off-diagonal, which is about cross-queue interaction. If you add one item to this queue, how much bump would it cause for the other queue next round? The server is involved in this calculation because what one queue takes the other loses due to the split of work at the server. The retrier is also involved because its pending count tracks the fresh queue, and the retries it sends land in the duplicate queue. The number $7/12$ consists of $1/2$ from the retrier (with $T=2$, one extra item in the fresh queue eventually produces one extra retry, but spread over two rounds) plus $1/12$ from the server. The other off-diagonal number $1/6$ is from the server alone, due to the extra duplicate diluting fresh's share of the S=3 capacity split.

Tracking down the Instability

The paper's small gain theorem suggests us to multiply the gains around the loop and check that the product is under one.

Let's choose the two entries on the off-diagonal of the table. These say that a longer fresh queue makes more duplicates ($7/12$, the effect of $f$ on next $d$) and more duplicates starve the fresh service ($1/6$, the effect of $d$ on next $f$). Since these involve the interaction of the two components, let's call that coupling.  When we multiply them, we get $\frac{7}{12} \cdot \frac{1}{6} = \frac{7}{72} \approx 0.1$. That says, a nudge sent once around the loop returns a tenth of its size. This says the system is stable with a factor of ten to spare. But it is wrong, because it reads only two of the four numbers in that table.

The two numbers on the diagonal, $11/12$ and $5/6$, describe the other side of the coin: How much of each queue is still there next round, with the other queue playing no part. Recall that both of these come from the server alone. Let's call this one memory. The small gain theorem reads only the coupling and ignores the memory.

When we take the memory into account, the real per-round multiplier becomes $1.19$, which is above one, so almost any disturbance grows rather than decays.

We get that number through standard linear stability analysis. We look for a nudge $(x,y)$ that the table just scales by some factor $r$. With entries $a,c$ on top and $b,d$ below, that means $ax+cy=rx$ and $bx+dy=ry$. When we solve each for $y/x$, set them equal, and we get the table's characteristic polynomial: $$r^2 - (a+d)\,r + (ad - bc) = 0$$

The two roots of a quadratic add up to the negative of the middle coefficient and multiply to the constant term. So our two factors (eigenvalues) add to $a+d$ (trace) and multiply to $ad-bc$ (determinant).

The trace comes from the diagonal only: $11/12 + 5/6 = 1.75$. Coupling shows up in the determinant as a subtraction: $0.76 - 0.10 = 0.67$.

If we drop the coupling, the determinant returns to $0.76$ with the trace unchanged, giving us $0.92$ and $0.83$, both under one. If we restore the coupling, the determinant falls to $0.67$, which splits the same sum into $1.19$ and $0.56$, where one factor is above 1, spelling trouble. 

This arithmetic also explains the two known fixes. A retry budget zeroes the $7/12$ entry; fresh-first service zeroes the $1/6$. Either way nothing is subtracted from the determinant and the factors fall back to $0.92$ and $0.83$. Each queue still carries over more than 80% of itself every round, but with no coupling to feed that carryover the backlog drains 8% a round instead of growing 19%.

Capping the queues is another version of the same move. A cap of $M$ on the fresh queue means the retrier can never emit more than $(M-6)/T$ retries, which is a hard ceiling on the $7/12$ coupling entry. This is a form of retry budget again. The backlog drains only if the ceiling sits under the headroom: at $M=7$ the cap allows zero retries and every start drains, while at $M=8$ it allows one retry, and other attractors start appearing in the space. Doing a simulation sweep shows that above $M=8$, the cap bounds the divergence but does not prevent the failure. Instead of growing without limit, the queues climb to the ceiling and stay. At $M=40$ the system parks at $(39,38)$: of the three units  served per round, one does useful work and two go to duplicates of requests already in flight. That is the very definition of metastability.

The Upshot

The parametric assume-guarantee paper gave me a better way to write a component's promise as a family of contracts indexed by how bad the environment is. But it did not give me a recipe for composition for practical systems. Since the paper's model is memoryless and uses one scalar, it didn't apply to our example. I got the four slopes by writing out how both queues evolve together, which meant abandoning composition for that step. However, it's worth noting that every term in that table comes from a single component, and the $7/12$ is just the retrier's $1/2$ added to the server's $1/12$. So there may be a way to work composition out here in the future.