Meine Suche nach einer prinzipienbasierten Lösung für metastabile Fehler hat mich zur Selbststabilisierung zurückgeführt. Ein kürzlich erschienenes Paper brachte das Problem mit der Komposition selbststabilisierender Systeme in Verbindung, aber die Literatursuche ergab nichts Nützliches. Geschichtete Stabilisierung war bereits Anfang der 2000er Jahre vorhanden, und seitdem scheint nichts Grundlegendes hinzugefügt worden zu sein.

Ich griff das Problem mit einem konkreten Beispiel an: einem Rely-Guarantee-TLA+-Modell eines Retry-Sturms als zwei Komponenten mit Verträgen. Dieses Modell reproduziert metastabile Fehler, weil die Komposition von guten Zuständen aus funktionierte, aber versagte, als ein großer Schock den Basisfall entfernte. Bei der Suche nach Rely-Guarantee-Komposition von jedem Zustand aus stieß ich auf ein regelungstheoretisches Paper von 2017 von Kim, Arcak und Seshia, „A Small Gain Theorem for Parametric Assume-Guarantee Contracts“. Dieses Paper tut ungefähr das, was ich will: zirkuläres Schließen zwischen zwei Komponenten ohne Schichtung oder Blockierung auflösen. Aber es hat ernste Einschränkungen. Eine Komponente ist eine Eingabe-Ausgabe-Relation auf Signalen, und Verträge beziehen eine Eingabegrenze auf eine Ausgabegrenze. Diese gedächtnislose Sicht kann den aus vorherigen Runden angesammelten Rückstand nicht ausdrücken, was Warteschlangen ausschließt. Sie hat auch keine Verbindung zur Stabilisierung.

Dennoch sind einige Teile es wert, für eine kompositionelle Theorie der Selbststabilisierung und Metastabilität gestohlen zu werden. Unten versuche ich, dies auszuarbeiten ... etwas erfolglos.

In unserem ursprünglichen Modell war die Garantie des Wiederholers bedingt: „Wenn die Warteschlange unter 6 liegt, sende ich keine Wiederholungen“. Die große Idee des parametrischen Assume-Guarantee-Papers ist es, eine Familie von Verträgen zu schreiben, die überall abdecken. Konstanten: S=3 Serverkapazität, A_max=2 neue Ankünfte, T=2 Timeout, Latenzschwelle S·T=6. Dies ergibt λ(L) = ⌊(L-6)/2⌋. Der alte Vertrag ist die oberste Zeile: λ(6)=0. Jede Zeile bekommt ein Versprechen, also erhalten wir ein Bündel gewöhnlicher Verträge, einen pro Schlechtigkeitsstufe p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). Die Annahmenseite ist eine Disjunktion, weil die Stufen Alternativen sind. Die Garantieseite ist eine Konjunktion; Verpflichtungen sind kumulativ. Zeilen, deren Bedingung falsch ist, kosten nichts; verschachtelte Stufen bedeuten, dass die strengste gewinnt.

Schlüsselentitäten: Personen: Kim, Arcak, Seshia