Exploring a Compositional Theory for Self-Stabilization and Metastable Failures

The Search for Compositional Self-Stabilization

The author's investigation into metastable failures led back to the concept of self-stabilization, specifically the composition of self-stabilizing systems. A review of recent literature revealed a lack of new fundamental contributions to this area since the early 2000s, with layered stabilization being the last significant development.

Addressing Metastable Failures with TLA+

To tackle the problem, the author used a concrete example: a rely-guarantee TLA+ model of a retry storm. This model, composed of two components with contracts, successfully reproduced metastable failure. The issue arose because the composition, which worked from stable states, failed when a large shock removed the underlying conditions that maintained the system's stability.

Parametric Assume-Guarantee Contracts

A search for rely-guarantee based composition from every state uncovered a 2017 control theory paper by Kim, Arcak, and Seshia titled "A Small Gain Theorem for Parametric Assume-Guarantee Contracts." This paper's approach to discharging circular reasoning between two components without layering or blocking aligns with the author's goals.

Limitations of the Parametric Approach

Despite its relevance, the parametric assume-guarantee approach has significant limitations. Its formalism treats components as memoryless input-output relations, making it unable to express concepts like accumulating backlog or queues, which are crucial in distributed systems. Furthermore, the paper does not connect to stabilization, lacking discussions on variant/potential functions or convergence reasoning. However, the author believes some elements of this work can still contribute to a compositional theory of self-stabilization and metastability.

Understanding Parametric Contracts

The core idea of parametric assume-guarantee contracts is to define a family of contracts that cover all possible states, rather than a single promise with a precondition. For example, instead of a conditional promise like "if the queue is under 6, I send no retries," a parametric contract would state, "Whatever the queue length L turns out to be, I send at most λ(L) retries." This provides a more comprehensive coverage of component behavior.