Metastability as a failed conditional discharge of rely-guarantee composition

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 fresh requests: the requests sent and not yet acked. A retry is a duplicate of a request already counted in p, so sending one does not grow p. The server has no private state, and does not know about p.

The constants in the specs parametrize the most important system characteristics:

• S=3 is the server capacity to process units per round
• AMax=2 is the max arrivals of fresh requests per round; retries arrive on top of this
• T=2 denotes retry timeout in rounds.

Since AMax<S, client demand stays below server capacity, so under normal conditions the server coasts. Whatever goes wrong will be due to a trigger/shock. Recall that metastability is a three act play: a trigger creates a backlog, the trigger goes away, but the system fails to recover. Since we only study the last act here, I model the trigger by starting the system in an already displaced state: Q0 requests are already queued at the server (qf=Q0) and, none being answered yet, all still open on the retrier's ledger (p=Q0). 

How does this initial shock then convert into retries? In my model, the retrier does not keep track of latency directly, rather it counts what it is waiting on, and Little's law turns the count into a duration. With p-done requests still unacked and S served per round, the wait is about (p - done)/S, so the timeout fires exactly when p-done>S*T. Let's call that LatThresh=6. The first LatThresh pending requests are deemed within their latency budget. But, anything beyond that has been waiting longer than T and gets retried, spread over the T rounds of the timeout period. This flux (recomputed each round from what is still pending) is the number of duplicates the retrier emits into qd (not qf) on its turn.

flux == NatSub(p - done, LatThresh) \div T

The server serves Min(S, qf + qd) units per round, split between the qf and qd classes in proportion to their queue sizes. Only a fresh request service gets an ack on done. That is, a request earns one useful ack no matter how many copies of it get served, and serving a duplicate is treated as pure waste. So these retries/duplicates add queue load without subtracting anything from p (pending requests), and this is what fuels the retry storm. 

The open specs and their relies

Each component is model-checked in isolation by using an "Env" stub for its partner.

The retrier's stub (=EnvS=) emulates a server that serves Min(S, qf+qd) units (split any way between qf and qd, when =S= is less than qf+qd), and acks fresh completions. Against this,  the retrier establishes its accounting invariant

PAcct == p = qf + done

PAcct says that the value of the client's ledger p for pending requests is equal to the server's fresh queue + the acks in transit. In turn, the retrier guarantees that it won't send retries while qf <= LatThresh, and that total queue growth per turn is bounded by AMax plus the flux. Note the wording: the retrier acts on p (the flux formula reads p-done), but it states its guarantees over qf, which its partner can see. PAcct is the bridge between the two: since p-done=qf under it, the flux can be rewritten as NatSub(qf,LatThresh)\div T, and the retrier's step implies the server's stub only under PAcct.

The server's stub (EnvR) emulates fresh arrivals of at most AMax, and retries of at most NatSub(qf, LatThresh)\div T ( the same flux again, in its qf form). Against this, the server guarantees a stability basin: if qf + qd <= LatThresh at a round start, it stays there, inductively, forever.

The composition and two scenarios

Compose.tla drops both of the Env stubs and conjoins the Retrier and Server actions together:

Next == Rt!RetrierTick \/ (Sv!ServerTick /\ UNCHANGED p)

Let's call qf + qd the backlog, all work queued at the server. We will use two properties over the backlog to frame our findings. The healthy states is Good == qf + qd <= S + AMax, a backlog of no more than one round's arrivals on top of what the server clears in a round. And stabilization is the property that the system eventually reaches Good and stays there, written <>[]Good. Secondly, Bounded == qf + qd <= 50 is a simple safety cap saying the backlog never blows past 50.

With these in hand, let's run two configurations on either side of LatThresh=6.

Q0 = 5, just inside of LatThresh. Everything passes, including stabilization. The reachable state space is small because inside the basin the retrier sends zero retries. So, the healthy case is trivial.

Q0 = 18, well outside of LatThresh. Here Bounded fails, and the violation trace shows a retry storm in action. 

The columns show that done collapses to 1 and stays there. The server does 3 units a round and gets only one useful completion, because the proportional split hands the rest to duplicates. Since p rises, flux stays at 6-7 a round.  The original stuck requests stay stuck in qf, and fresh arrivals add 1-2 items per round as well. Unfortunately, the system generates three times more load from its own retries than from its customers.

Why do the discharge proofs not help here? It's because both guarantees carry an "if". The retrier promises no retries if qf<=LatThresh. The server promises that the stability basin holds if retries are bounded. At Q0=5 the two conditions hold each other up through a circular induction with a base case. At Q0=18 both implications are still true, but since there are conditional guarantees, they just never apply since the base case is missing. 

Mapping the basin

The two runs above are two samples of a function from Q0 to a long-run outcome. We can sweep Q0 to see the whole picture, but first let's give precise definitions to explain the outcomes better.

We have already seen the good outcome, guaranteed recovery, the property <>[]Good that passed at Q0=5. A companion check confirms that from Q0=5 no reachable state is one of permanent failure.

The bad outcome is *permanent failure*: a state from which no continuation ever recovers. To certify it we need a concrete region of such states: Trapped == qf >= 8*S  /\  qd >= 3*qf

How would qf, the fresh queue, get this large? With qd>=3*qf, duplicates own at least three quarters of the queue, so fresh work's share of the proportional split rounds down to zero, and all three units of capacity go to duplicates, every round. Since qf receives up to AMax arrivals per round and loses nothing, the fresh queue creeps up, even though the server capacity S=3 exceeds max fresh arrivals AMax=2. 

A large =qf= is what keeps the trap fed. Zero fresh service means done=0, so by PAcct the pending ledger is p=qf. With qf >= 8*S =24, the flux is (24 - 6) \div 2 = 9 duplicates per round which swamps the 3 the server drains per round and this causes qd to grow three times faster than qf grows. The server runs at 100% utilization and accomplishes nothing useful, forever. Note that Trapped is a conservative region: it does not cover every doomed state (the sweep below finds dooming displacements well outside it), but it is a region where doom is provable by closure. 

To show this more formally, we show two things. First, the trap is reachable: from Q0=30, assert ~Trapped as an invariant and TLC violates it -- the trace is the descent into the trap. Second, the trap is closed: for this, set Init=Trapped, so every trapped state is a start state, and verify no execution leaves the Trapped state. Reachable plus closed is an impossibility certificate built from two invariant checks.

"Does Q0 recover?" is the stabilization check: does =<>[]Good= hold? And "Is =Q0= doomed?" is the reachability check: assert ~Trapped as an invariant and see whether TLC finds a path into the trap.  So the sweep is a for-loop that runs both checks at each Q0.

Our two example runs were rows one and three: Q0=5 recovers, Q0=18 is doomed. The middle band, where neither fate applies, is worth exploring.

In the middle band Q0= 7..9 the stabilization property fails: under sustained load the backlog neither drains nor explodes, since inflow (2 arrivals + 1 retry) exactly matches capacity 3, and the system orbits forever. But the trap is unreachable, and an additional check shows recovery is still possible. If we restrict fresh arrivals to zero, <>Good passes. 

The same quiet-recovery check also passes at Q0=10,15,20, displacements from which the trap is reachable. There is no contradiction here though. These states are not in the trap (that needs qf >= 24, qd >= 72), the trap is merely downstream of them. "Trap reachable" says some continuation falls in. "Quiet recovers" says the continuation that cuts arrivals does not get captured by the trap. Above Q0=10 you are at the risk of getting trapped, but if you shed load now, you can stay out.

Note that "quiet" stops fresh arrivals, but the retries keep firing, since flux is driven by p, not by new traffic. Quiet works before the trap because with no new arrivals the fresh queue drains, acks flow, p falls, and the flux dies out on its own. Inside the trap that path is long gone: fresh service is starved to zero, so p never falls and the retries feed themselves regardless of arrivals. To act on the retries directly you need a different lever, capping the retry flux itself. That is the fix below, and unlike quiet it works from every state.

Fixing the retry law

The fix is to give the retrier a budget B. This is a hard cap on how many retries it may emit per round, no matter how large its pending backlog grows. (This is the token bucket/retry circuit breaker approach that production SDKs already implement.) In the spec this is a one-line change to the flux rule:

flux == Min(rawflux, B)

Choose B so that AMax+B < S. Then the total inflow per round, arrivals plus retries, is below the server's capacity in every state, not just inside the basin. This removes the "if" from the stability argument: the basin guarantee was conditional on retries staying bounded, and now they always are. A check with TLC confirms that stabilization holds from =Q0 = 30=, deep in trap territory.

The TLC results hold at S=3, AMax=2, T=2, but I also got Claude Code write TLAPS proofs of the discharges and the basin induction, checked with tlapm, which lift them to all parameter values. The two basin theorems make the fix visible as a deleted assumption: the uncapped one requires Q0 <= LatThresh as an explicit hypothesis, the budgeted one holds with no hypothesis on Q0.

There is a second fix, from the server's side, and it may be the better one. The trap has two root causes: unbounded retries and the proportional split, and removing either dissolves it. If we swap the server to fresh-first service, the trapped states drain with no client change at all. The mechanism has two phases: fresh work is now served at full capacity, so acks start flowing, and p keeps decreasing, which drains the flux. After that, the leftover capacity chews through the accumulated qd. TLC confirms recovery from the deepest corner of the trap (qf=30, qd=120), in about 70 rounds. The retrier's guarantees survive the swap (its rely never depended on a specific split policy). The server-side fix also scales where the budget approach fails: with =N= clients each holding budget B, safety needs N * (AMax + B) < S, whereas one fresh-first server protects itself against any number of clients.

Conclusion: did composition matter?

Would a monolithic spec have found the storm just as well? Yes, but what the compositional framing put on the table is the contract itself. In our runs, the storm sustained itself while every contract check kept passing: the system failed with no component at fault. That observation cannot even be stated without making the contracts explicit. And once we state the contracts, we zero in on the problem. Both original guarantees were conditional, holding only inside the basin. Both of our fixes were contract edits: the retry budget strengthens the retrier's guarantee to "at most B retries, from every state", and fresh-first strengthens the server's, letting each partner's rely hold unconditionally. The monolithic model shows the backlog grows, whereas the compositional one is needed to show which promise was too weak, and strengthening that promise is the fix.

Specs and configs are available here: https://github.com/muratdem/retry-stab-modular-spec