自己安定化の構成理論を探して

メタステーブル障害に対する原理的な解決策を模索する私の探求は、最近の論文がこの問題をセルフ・スタビライゼーション・システムの構成に関連付けていたことから、セルフ・スタビライゼーションのルーツへと私を連れ戻しました。しかし、セルフ・スタビライゼーション・システムの構成に関する最近の研究の文献調査では、有用なものは何も得られませんでした。レイヤード・スタビライゼーションの考え方は2000年代初頭にはすでに確立されており、それ以降、根本的な進歩は見られないようです。フラストレーションが溜まります。

そこで、手元にある具体的な例を使って問題に取り組むことにしました。リトライ・ストームのリライ・ガーアンティ TLA+ モデルを、契約を持つ2つのコンポーネントとして構成しました。そのモデルはメタステーブル障害を再現します。なぜなら、正常な状態から機能した構成が、基盤となっていたケースを大規模なショックが取り除いたときに機能しなくなったからです。

すべての状態からのリライ・ガーアンティに基づく構成を検索したところ、Kim、Arcak、Seshia による2017年の制御理論の論文「A Small Gain Theorem for Parametric Assume-Guarantee Contracts」が見つかりました。この論文は、私が望んでいることに近いことを行っています。レイヤリングやブロッキングなしに、2つのコンポーネント間の円環的推論を解消します。しかし、いくつかの深刻な制限があります。彼らのフォーマリズムでは、コンポーネントはシグナル上の入出力関係であり、契約は入力バウンドと出力バウンドを関連付けます。これはコンポーネントのメモリレスな見方であるため、前のラウンドから蓄積されるバックログを表現することはできません。これにより、キューなどの有用な分散システム概念が除外されます。また、スタビライゼーションとの関連もありません。この論文では、バリアント/ポテンシャル関数や収束推論については言及されていません。しかし、セルフ・スタビライゼーションとメタステービリティの構成理論に向けて盗む価値のある断片はまだあります。以下に、ある程度成功せずに、それを展開しようと試みます...

パラメトリック・アシューム・ガーアンティ契約の理解

元のモデルでは、リトライヤーの保証は条件付きかつ部分的でした。「キューが6未満なら、リトライは送信しない」。この契約は、キューが18の場合については何も述べていません。「if」条件が満たされないため、約束は虚偽充足され、コンポーネントは何も負いません。

パラメトリック・アシューム・ガーアンティ論文の大きなアイデアは、前提条件を持つ単一の約束を書くのではなく、すべてをカバーする契約のファミリ全体を書くことです。

疲れた: キューが6未満なら、リトライなし。

配線済み: キューの長さ $L$ がどうであれ、送信するリトライは $\lambda(L)$ 以下とする。

モデルからの定数は、$S=3$（サーバー容量/ラウンド）、$A extsubscript{max}=2$（最大新規到着/ラウンド）、リトライ・タイムアウト $T=2$（レイテンシ閾値 $S \cdot T = 6$）です。これにより、$\lambda(L) = \lfloor (L-6)/2 \rfloor$ となり、以下のようになります。

古い契約は、一番上の行としてまだ含まれています。$\lambda(6)=0$ は「キューが6未満なら、最大ゼロリトライ」と言っています。古い契約はキュー長18では無効ですが、パラメトリック化されたアシューム・ガーアンティアプローチの下では、テーブルの各行が約束を得ます。したがって、悪いレベル $p$ ごとに1つの通常の契約のバンドが得られます。

$$\varphi extsubscript{a} = \bigvee extsubscript{p} \psi extsubscript{a}(p)$$

$$\varphi extsubscript{g} = \bigwedge extsubscript{p} \left( \psi extsubscript{a}(p) \Rightarrow \psi extsubscript{g}(\lambda(p)) \right)$$

前提条件側、$\varphi extsubscript{a}$ は、レベルが代替であるため、選言です。環境は、それが偶然発生するいずれかのレベルになります。「キューが6以下、または8以下、または10以下、または...」は、実質的にあらゆる環境によって満たされるため、外に出るエンベロープは残っていません。

保証側、$\varphi extsubscript{g}$ は、同じレベルでの連言です。義務は累積的であるため、すべてを一度に負います。条件が偽である行はコストがかからず、レベルはネストされているため、複数の条件が同時に適用され、最も厳しいものが勝ちます。キューが7の場合、「8以下」が適用され、コンポーネントは最大1リトライを負います。「10以下」も適用され、最大2を負いますが、最初のケースはすでにそれを意味しています。単調性がここで鍵となります。

スモールゲインルールの導出

このようなループが収束するルールは何でしょうか？論文ではこれをスモールゲイン定理と呼んでいます。直感から説明を始めましょう。

この現象を見たことがあるでしょう？マイクがスピーカーの前に来ると、マイクが音を拾い、アンプがそれを増幅します。スピーカーがそれを再生し、マイクが再びそれを拾います。ループを一周するたびに音が倍増し、甲高いスキール音が聞こえます。

このプロセスを定量化するには、コンポーネントごとに1つの数値が必要です。つまり、入力あたりの「悪さ」の出力です。これはコンポーネントの応答関数の傾きであり、制御理論ではコンポーネントのゲインと呼びます。

2つのコンポーネントをチェーンし、最初のコンポーネントに摂動 $x$ を入力し、傾き $g extsubscript{1}$ があり、$g extsubscript{1} x$ が出力されるとします。それを2番目のコンポーネントに入力し、傾き $g extsubscript{2}$ があり、$g extsubscript{2} g extsubscript{1} x$ が出力されるとします。1周すると、摂動は $g extsubscript{1} g extsubscript{2}$ 倍になります。積が1未満なら、周回は幾何級数的に縮小し、ループは収束します。1を超えると、発散します。証明は幾何級数からです。

スモールゲイン定理は非常にエレガントで、すべての開始状態を一度にカバーするグローバルな結果をもたらします。しかし、スモールゲインのセットアップには限界があります。この場合、2つのことがこのショートカットの使用を妨げます。

第一に、これには直線が必要です。私たちのリトライヤーは直線的な傾き $1/2$ を持ちますが、サーバーはそうではありません。そのサービスシェアは $f/(f+d)$ として計算されるため、その傾きはキューの場所によって異なります。したがって、単一の数値を掛けることはできません。

第二に、そしてさらに悪いことに、ショートカットは悪さを1つの数値として仮定します。私たちのシステムには、異なる動作をする2つのキューがあります。新規ワーク $q extsubscript{f}$ と重複 $q extsubscript{d}$ です。一方のバウンドはもう一方のバウンドではありません。したがって、ループの1周は数値のペアを数値のペアにマッピングします。

両方の制限の下には、導入で私が不満を述べたコンポーネントのメモリレスな見方があります。このセットアップでは、ゲインは入出力関係です。それは、どれだけ多くのものが渡されるかを示します。前のラウンドからまだ残っている自分のバックログの量のためのスロットはありません。キューは主にバックログであり、それが次のセクションで扱う内容です。

2つのキューと4つのスロープの処理

両方のキューを追跡しましょう。新規キュー $f$ と重複キュー $d$ のペアに対するラウンドを、到着の適用、リトライの適用、比例サービス分割の適用によって次のペアを決定するルールとして記述できます。次に、どのペアがそれ自身にマッピングするかを尋ねます。

1つのペアがそうなります: $(f,d) = (8,4)$。ここで合計キューは12なので、3単位の容量は新規に2、重複に1を分割します。2つの新規サーブは2つの到着と正確に相殺されます。リトライ率は $(8-6)/2 = 1$ で、1つの重複サーブがそれを正確に相殺します。したがって、次のラウンドでは、キューはバランスを保ちます。

問題は、このバランスポイントの近くから開始した場合に何が起こるかです。$(9,4)$ から開始した場合、システムは元に戻るのか、それとも暴走するのか？これを答えるには、小さな摂動がどのように伝播するかを知る必要があります。

計算は省略しますが、これがテーブルです。

対角線から始めましょう。ここでは、キューに1つのアイテムを追加した場合、次のラウンドでそのキューがどれだけ大きくなるかを推論します。この推論では、サーバーのみが関与し、$11/12$ と $5/6$ を得ます。これらは、そのアイテムのどれだけが次のラウンドでまだ残っているかの割合です。

次に、オフ対角線、つまりキュー間の相互作用について考えます。このキューに1つのアイテムを追加すると、次のラウンドで他のキューにどれだけ影響を与えるでしょうか？サーバーは、一方のキューが消費するものが、サーバーでの作業の分割により他方が失うため、この計算に関与します。リトライヤーも関与します。なぜなら、その保留中のカウントは新規キューを追跡し、送信するリトライは重複キューに着弾するからです。数値 $7/12$ は、リトライヤーからの $1/2$（$T=2$ で、1つの追加アイテムが新規キューに最終的に1つの追加リトライを生成しますが、2ラウンドにわたって分散されます）とサーバーからの $1/12$ から構成されます。もう一方のオフ対角線の数値 $1/6$ は、サーバーのみからのもので、追加の重複が $S=3$ 容量分割の新規のシェアを希釈するためです。

不安定性の追跡

論文のスモールゲイン定理は、ループ内のゲインを掛け合わせて1未満であることを確認することを提案しています。

テーブルのオフ対角線の2つのエントリを選択しましょう。これらは、長い新規キューがより多くの重複を作成すること（$7/12$、次の $d$ への $f$ の影響）と、より多くの重複が新規サービスを枯渇させること（$1/6$、$f$ への $d$ の影響）を示しています。これらは2つのコンポーネントの相互作用を含むため、これをカップリングと呼びましょう。それらを掛け合わせると、$\frac{7}{12} \cdot \frac{1}{6} = \frac{7}{72} \approx 0.1$ になります。これは、ループを1周した摂動がそのサイズの10分の1で返ってくることを意味します。これは、システムが10倍の余裕を持って安定していることを示しています。しかし、それは間違っています。なぜなら、テーブルの4つの数値のうち2つしか読んでいないからです。

対角線の2つの数値、$11/12$ と $5/6$ は、もう一方の側面を表しています。他のキューが関与しない場合、各キューのどれだけが次のラウンドでまだ残っているかです。両方ともサーバーのみから来ていることを思い出してください。これをメモリと呼びましょう。スモールゲイン定理はカップリングのみを読み取り、メモリを無視します。

メモリを考慮に入れると、実際の1ラウンドあたりの乗数は $1.19$ になり、1を超えているため、ほとんどの摂動は減衰するのではなく成長します。

この数値は標準的な線形安定性解析を通じて得られます。テーブルが単にいくつかの係数 $r$ でスケーリングする摂動 $(x,y)$ を探します。上部にエントリ $a,c$、下部に $b,d$ がある場合、$ax+cy=rx$ および $bx+dy=ry$ となります。それぞれを $y/x$ について解き、それらを等しくすると、テーブルの特性多項式が得られます。
$$r^2 - (a+d),r + (ad - bc) = 0$$

二次方程式の2つの根は、中間の係数の負の数と等しく、定数項と等しくなります。したがって、2つの因子（固有値）は $a+d$（トレース）と等しくなり、$ad-bc$（行列式）と等しくなります。

トレースは対角線のみから来ます: $11/12 + 5/6 = 1.75$。カップリングは行列式に減算として現れます: $0.76 - 0.10 = 0.67$。

カップリングをドロップすると、行列式は $0.76$ に戻り、トレースは変更されないため、$0.92$ と $0.83$ になり、どちらも1未満です。カップリングを復元すると、行列式は $0.67$ に低下し、同じ合計を $1.19$ と $0.56$ に分割します。ここで1つの因子は1を超えており、問題が発生します。

この計算は、2つの既知の修正方法も説明しています。リトライ予算は $7/12$ のエントリをゼロにし、新規優先サービスは $1/6$ をゼロにします。どちらの場合も行列式から何も引かれず、因子は $0.92$ と $0.83$ に戻ります。各キューは毎ラウンド80%以上を保持しますが、その繰り越しを供給するカップリングがないため、バックログは19%成長するのではなく、毎ラウンド8%ずつ排出されます。

キューのキャッピングは、同じ操作の別のバージョンです。新規キューに $M$ のキャップを設けるということは、リトライヤーが $(M-6)/T$ リトライを超えることはできないことを意味します。これは $7/12$ のカップリングエントリに対するハードシーリングです。これはリトライ予算の一種です。バックログは、シーリングがヘッドルームの下にある場合にのみ排出されます。$M=7$ ではキャップはリトライをゼロにし、すべての開始が排出されますが、$M=8$ では1リトライを許可し、他のアトラクターが空間に出現し始めます。シミュレーションスイープを行うと、$M=8$ を超えると、キャップは発散を制限しますが、障害を防ぐことはできません。キューは無限に成長するのではなく、シーリングに達して留まります。$M=40$ では、システムは $(39,38)$ で停止します。毎ラウンド提供される3単位のサービスのうち、1単位は有用な作業を行い、2単位は処理中のリクエストの重複に費やされます。これはメタステービリティの定義そのものです。

要点

パラメトリック・アシューム・ガーアンティ論文は、環境の悪さによってインデックス付けされた契約のファミリとしてコンポーネントの約束を記述するためのより良い方法を提供してくれました。しかし、実用的なシステムのための構成レシピは提供してくれませんでした。論文のモデルはメモリレスであり、単一のスカラーを使用するため、私たちの例には適用できませんでした。両方のキューがどのように進化するかを書き出すことで4つのスロープを取得しましたが、そのステップでは構成を放棄する必要がありました。しかし、そのテーブルの各項は単一のコンポーネントから来ており、$7/12$ はリトライヤーの $1/2$ にサーバーの $1/12$ を加えたものであることに注意する価値があります。したがって、将来的にはここで構成を機能させる方法があるかもしれません。