分散システム一貫性テストフレームワーク Jepsen の Nuwa での実用化

[[431416]]

Nuwa チームは、過去 6 か月間にわたって Nuwa 2.0 の研究開発に投資を続け、一貫性エンジンとビジネス ステート マシンを切り離してきました。整合性エンジンは、Paxos、Raft、EPaxos などの複数の整合性プロトコルをサポートし、ビジネス ニーズに応じてさまざまなビジネス ステート マシンをサポートできます。一貫性エンジン モジュールが鍵となります。整合性エンジンを開発する際には、整合性エンジンの正確性を確保することが大きな課題となるため、TLA+ や Jepsen などのツールを使用して整合性エンジンの正確性を確保しました。ここでは、Jepsen を適用した私の経験をいくつか紹介したいと思います。

インターネット上には「Jepsen Test」や「When Messaging Meets Jepsen」など、Jepsen の紹介書がすでに存在しており、原理や使い方を詳しく説明しており、広範かつ詳細に解説されています。ジェプセンについて包括的に理解するために、まずこれらの記事を読んでください。また、詳細がわからない場合は、記事内の詳細な説明を読むこともできます。この記事は、要約、概要、補足に相当します。一方で、ジェプセンについて直感的に理解できるようになります。一方、Jepsen の役割と特徴を実際に説明するために、Nuwa が Jepsen を使用している例を紹介し、Jepsen を実際に使用するための参考資料を提供します。

ここでは、ジェプセンについて、本質、構造、機能の順に簡単に説明します。

1. エッセンス - ジェプセンの特徴だけを見る

分散システムテストの分野では、TLA+ と Jepsen という 2 つのツールが最もよく知られています。それらの関係は演繹と帰納、ホワイトボックスとブラックボックスに似ています。 TLA+ では、テストを作成する人が検証する必要のある分散システムを真に抽象化し、あらゆる微妙な論理部分で実際のシステムを簡潔かつ正確に復元し、さまざまな状態空間でこの抽象システムを走査できることが求められます。抽象システムが定義されたルールを常に満たしていることが検証されれば、実際のシステムの正しさを推論し保証することができます。詳細な重要な情報が記載された地図を持っていて、その地図上にルートを描くようなものです。現実世界でもルートを辿ることで目的地に到着することができます。ジェプセンは、システムが外部に提供するインターフェースから始めます。実際にシステムを構築し、操作を実行し、エラーを注入し、その結果を検証するなど、エラー注入条件下でのシステムの動作に関する一連の訓練と分析を通じて、確立されたルールに準拠しない状況に実際に遭遇します。これらの状況は歴史的記録の分析を通じて発見されます。それは、散らばったパズルをたくさん作り、さまざまなことを試し、最終的にそれらを組み合わせれば合理的で規則的なパターンになるかどうかを検証するようなものです。

このことから、両方の難しさが容易にわかります。 TLA+ の難しさは、推論の正確さにあります。 TLA+ で記述されたモデルは、抽象システムが実際のシステムの主要部分と完全に一致しているという前提に基づいています。エンジニアリング実装と一致していない場合、実際のシステムで発生する可能性のあるいくつかの問題を検証できません。 Jepsen の最大の難しさは、テスト ケースで収集された履歴記録に基づいて、システムに対応するエラーがあるかどうかをどのように要約するかです。さらに、要約自体の特性により、Jepsen テストではすべての異常な状況をカバーできないことも判明します。この帰納的プロセスにおいて、線形一貫性は帰納的に検証するのが最も難しく、システムの線形一貫性の検証は Jepsen の最大の特徴でもあります。

図1. Jepsenが提供する一貫性検証機能

一言で言えば: Jepsen ≈ マルチプロセステストプログラム + 線形化可能性検証

• マルチプロセステストプログラムの目的は、さまざまな状況下でのシステムの動作記録を生成することであり、線形一貫性検証は動作記録を確認することです。 Jepsen は、ノード上で複数のクライアント スレッドを開始し、テスト対象のシステムにさまざまな要求を送信し、要求結果を収集して各要求操作の記録を作成するブラック ボックス テストです。通常、システム上で同様のテストが行​​われます。比較すると、Jepsen は、後続の分析のために操作記録を整理する部分を History に追加します。
• 線形一貫性の検証は、Jepsen テストと Failover テストの最大の違いです。 Jepsen は他の非線形一貫性検証も実行できますが、これらのテストは線形一貫性検証に比べて比較的単純で直感的であるため、この記事では主に線形一貫性検証について詳しく説明します。主な内容は次の 2 つの問題です。
  • 線形化可能性とは何か
  • さまざまな異なるシステムの検証を線形一貫性の検証に統合する方法。

1. 線形化可能性

前述の記事では、線形一貫性に関する非常に詳細な論文資料と直感的な説明が提供されており、学習することができます。この記事では、順次一貫性と線形一貫性の直感的な例を示します。

図2 順序的一貫性と線形的一貫性

順次一貫性と線形一貫性の最も重要な違いは、異なるクライアント間の操作間に明確な事前発生関係があるかどうかにあります。

Jepsen のすべてのクライアントは同じノード上にあるため、システム時間 (ロールバックなし) を使用して、クライアントから要求が送信されてからクライアントが応答を受信するまでの時点 (図の四角形の左端と右端に対応) を記録できるため、2 つの操作間に直接的な事前発生関係があるかどうかを確認できます。ある操作の終了時刻が別の操作の開始時刻より前である場合、2 つの操作には明確な先行発生関係があります。 2 つの操作の四角形がタイムライン上で重なる場合、それらの先行関係は平行であり、順序は不確定です。線形一貫性システムでは順序を任意に調整できます。

図 2 に示すように、Get2 は Set2 が要求を送信する前に応答を受信します。明確な事前発生関係がありますが、セット内のデータをそれ自身より前に取得できるため、線形一貫性に違反します。 Set3 操作と Get2 操作は並列ですが、順序に関係なく、線形一貫性を満たすシーケンスを形成することはできません。

左の図の順序一貫性が異なります。 P1 と P2 は異なるノードのクライアントである可能性があるため、それらの操作はタイムライン上で同じ参照を持ちません。したがって、同じクライアント上の操作が厳密な事前発生関係を持つようにすることだけが必要です。したがって、配列によって順序一貫性を満たすシーケンスが得られます。

2. 線形化可能性とジェプセン検証

Jepsen はモデルを使用して線形一貫性を検証します。モデルはステートマシンであり、Jepsen テストによって生成される履歴は入力のログです。ログ間には、先行関係と並列関係が存在します。 Checker が行う必要があるのは、happen-before 制約に違反することなく、毎回ログを適用した後で状態マシンが正しい動作を維持できるように、正しいログ順序を見つけることです。一度違反すると、システムが線形一貫性を満たしていないという証拠が見つかります。

Jepsen には、register/cas-register/multi-register/set/unordered-queue/fifo-queue などの組み込みモデルがあります。

たとえば、実装した分散ロックをテストする場合、Lock と Unlock という 2 つの操作があり、cas-register を直接適用できます (ここでは説明のために、実際には mutex が使用されています)。ロックが正常に取得されるたびにレジスタ 0 が 1 に設定され、ロックが正常に解放されるたびにレジスタ 1 が 0 に設定されます。そして、事前発生条件が満たされた場合、ログをどのように配置しても正しいステート マシン出力が得られない場合 (下図の左側に示すように)、実装された分散ロックが線形一貫性を満たしていないことを意味します。

図3 線形一貫性に準拠した履歴の例

上記の P1 と P2 の操作はすべて成功を返すものと想定します。左の図の可能なシーケンスをモデルに入力します。

右の図では、P2 Lock 操作と P1 Unlock 操作が並列であるため、History は Seq3 順序を持つことができます。

テストする他のシステムや機能についても同様です。線形一貫性を満たす条件下では、履歴にはさまざまなログ配置が可能です。履歴が任意の順序でモデルに入力されると、モデル自体の制約を満たすことができず、システムが線形一貫性を満たしていないことが証明されます。実際、Jepsen の線形一貫性ソリューションで使用される knossos は、すべての順列とトラバーサルをこの方法で実行するわけではありません。使用される特定の線形化可能な検証アルゴリズムは WGL であり、「線形一貫性理論」で参照できます。

2. 構造 - ジェプセンを分解して使用する

• 分散システム環境の構築
• 分散システム上で一連の操作を実行する
• 操作履歴記録を収集し、操作結果が期待どおりであることを確認します。

必要に応じて視覚化して、システムのパフォーマンスと可用性を反映するグラフを生成し、挿入されたエラーに対するシステムの応答を直感的に説明できます。

リファレンスの Jepsen テストの 3 つのステップは、Jepsen 構造の DB、Generator、および Checker モジュールに対応しています。 1.1 で Jepsen の本質を理解しても、実際の実践では、Jepsen を使用するべきかどうか、Jepsen をどのように使用すればよいかなど、まだ混乱するかもしれません。これらの質問に答えるには、まずジェプセンの構造から始める必要があります。前述の定義によれば、Jepsen = マルチプロセス テスト プログラム + 線形一貫性検証となります。必要に応じてJepsenを分解して使用することができます。我々はできる

• すべてのテストケースはJepsenを使用して書かれています
• 独自のテスト フレームワークを使用して、Jepsen に似た形式で履歴を生成し、それを Jepsen バリデーターまたは独自のバリデーターに置き換えることもできます。

図4. ジェプセンモジュール図

TIDB の chaos と同様に、Jepsen 関数のテスト フレームワークは、Go と線形一貫性検証ツールである porcupine を使用して Go で再実装されており、Jepsen と同じテスト効果を実現できます。実際には、どちらのソリューションでも機能を実現できますが、テクノロジを選択する際には、次の点を考慮する必要があります。

表1. ジェプセンテストの練習問題の選択

実用的な観点から、私たちは一方では検証の有効性、他方ではテスト作成の難しさに配慮しています。

テストの有効性は主にフレームワークの豊富なテスト機能によって保証されますが、作成の難しさはプロジェクトの効率と規模に直接影響します。オープンソースフレームワーク Jepsen を直接使用する理由は、機能が充実しており、認知度が高いためです。新しいフレームワークを構築すると、大規模なテストやケースの記述を簡単に開始できるようになります。同時に、言語の特性に基づいて、特定のテスト シナリオ (OOM の解決や既存のテスト フレームワークのコードの直接再利用など) により適している場合もあります。

したがって、システムの線形一貫性と、Jepsen が提供するその他の検証モデル (レジスタ/cas-register/multi-register/mutex/set/unordered-queue/fifo-queue などを含む) のみをテストする必要がある場合は、簡単にするために、Jepsen のモデルを直接適用できます。独自のシステムが提供するインターフェースを、既存の検証モデルの操作と同等のセマンティクスにカプセル化することで、検証に Jepsen を直接使用できるようになります。システム機能が既存の Jepsen テストと一致しており、システムのさまざまな機能を迅速にテストできる状況に適しています。

新しいテストを定義するシナリオが多数ある場合、または機能豊富なテスト フレームワークがすでに蓄積されている場合、またはチームが迅速かつ簡単に使用できるツールが必要な場合は、新しいフレームワークを構築する方が効率的なオプションです。 Clojure をすべての人に普及させたり、使いやすいテンプレートを提供したりするのではなく、古いハンマーを使って新しい釘を打つ方が便利です。

3. 機能 - ジェプセンを使ったヌワの例

その本質と構造を分析すると、Jepsen が一貫性のテストと検証に限定されず、その最大の特徴が線形一貫性にあることが容易にわかります。したがって、線形一貫性の保証を必要とするあらゆるシステムで、Jepsen の線形一貫性検証機能を使用できます。一貫性プロトコルに基づく分散ロックや分散キュー、あるいは MySQL のようなマスター スレーブ レプリケーション データベースなどです。

カスタム テストに Jepsen を直接使用する場合、作業は 2 つの部分に分かれます。

1) パッケージインターフェース

2) モデルとチェッカーをカスタマイズする

システム インターフェースは固定されているため、Jepsen にパッケージ化できます。インターフェースをパッケージ化するときは、インターフェースが応答を迅速に受信し、操作にかかる時間を短縮できるように注意してください。操作に時間がかかりすぎると、もともと特定の happen-before 関係にあった多数の操作が並列化され、不要な計算が大幅に増加し、OOM 問題が発生しやすくなります。たとえば、curl や Clojure の http ライブラリを使用して RESTful インターフェースを呼び出す場合、検証効率はまったく異なります。

最大の作業負荷は、システム固有のステートマシンに適応するためにモデルとチェッカーを変更することです。次に、Nuwa の RESTful 分散ロックの相互排除と可用性検証について紹介します。理解を深めるには、etcd の RESTful ロック インターフェースを参照してください。 Jepsen には、etcd の分散ロック テストなど、ロックの排他検証の例がいくつかあります。 Nuwa のインターフェース呼び出しに従って、acqure と release を同様に実装するだけです。ハートビートを停止した後、タイムアウト期間内にロックを取得できる他のクライアントが存在するかどうかなど、ロックの可用性をテストする場合は、モデル部分とチェッカー部分に対応する変更を加える必要があります。

1. カプセル化インターフェース

実施された操作は以下の通りです。各操作に含まれるインターフェースと関数は順番に呼び出されます。

表2. RESTfulロックテストインターフェースのカプセル化

これら 4 つの操作の処理をクライアント - LinearizableLockClient にカプセル化し、クライアント内で各操作の戻り値の処理を追加し、成功、失敗、タイムアウトの 3 つの状況に応じて、履歴内に各操作応答のログを生成します。このようにして、カプセル化されたインターフェースの操作が完了します。以降の実行では、Jepsen は確立されたルール (ランダム、時間指定など) に従って各操作を呼び出します。 aquire release のみが呼び出された場合、Checker はデフォルトの mutex チェッカーを使用して相互排他性を検証します。すべてが呼び出されると、カスタム チェッカーを使用して可用性が検証されます。

2. カスタムモデルとチェッカー

ロックを検証すると、モデル部分は引き続き Jepsen によって提供されるミューテックスを使用します。実際、Jepesen で取り上げられているモデルは、基本的にほとんどのシナリオをカバーしています。knossos の model.clj を参照してください。ロックを検証するために使用するミューテックスは次のとおりです。

 (defrecord Mutex [ロックされていますか?]
  モデル
  （ステップ[r op]
    (条件 = (:f ​​op)
      :acquire (ロックされている場合?
 「エラー: ロックされていますが、まだ利用可能です」  
                 （ 「すでに保有」は矛盾している）
                 (ミューテックス。true ))
      :release (ロックされている場合?
                 (ミューテックス。false )
 「エラー: ロックは保持されていませんが、解除できます」  
                 （ 「開催されていない」という矛盾）））） 
 
  物体
  (toString [this] (ロックされている場合? "locked"   "無料" ））） 
 
 「初期化中にロックが解除されました」  
 (ミューテックスの定義
「:acquire および :release メッセージに応答する単一のミューテックス」  
  []
  (ミューテックス。false ))

Mutex は Model を継承し、通常のロックと解放の各操作に応じて自身のステータスを更新していることがわかります。ロックをまだ取得できる場合、またはロックを保持せずに解放できる場合は、不整合があり、モデルの実行が失敗することを意味します。

チェッカー部分は、ロックの可用性を確認するための鍵となります。確認したいのは、リースの有効期限が切れる前、つまり touch-lease 間隔中にロックが奪われず、タイムアウト時間 (lease-ttl) 後にロックが奪われる可能性があることです。したがって、既存の履歴に基づいて仮想クライアントを作成します。開始時刻は release-lease 操作のleasing-ttl 時刻より後になり、release 操作が実行されます。プロセス中に別のクライアントによってロックが再度取得されるか解放されると、この仮想クライアントの操作は履歴でキャンセルされます。これにより、線形一貫性チェッカーを使用して Mutex モデルを検証し、ロックの可用性を証明し続けることができます。ロック ハートビートの有効期限が切れる前に他のクライアントによってロックが奪われることはなく、ロックのリースの TTL が終了した後にロックが奪われる可能性があります。ロックのリリース時間は動的な範囲であるため、リリースの開始時間と終了時間間隔がこの動的な範囲に追加されます。実際の変換効果は下図の通りです。

図5. ロック可用性テストの履歴遷移

このことから、モデルとチェッカーの変換は非常に柔軟かつ多様であることがわかります。履歴を取得したら、ビジネス ステート マシンに応じてモデル実行ログの結果を調整したり、履歴自体を処理していくつかの拡張シナリオに対処したりできます。線形一貫性を検証せず、他の機能 (結果一貫性、監視など) を検証する場合は、履歴を直接分析することもできます。結果一貫性では、すべての操作が完了した後にレジスタの読み取り結果が同じであることが要求され、監視では、各クライアントの監視結果によって結合されたシーケンスが一貫していることが要求されます。これらは比較的簡単に実装できる操作です。

IV.結論

最後に、Jepsen の使い方をまとめます。

TLA+ と比較すると、Jepsen は独自の分散システムをテストする際に使いやすいです。線形一貫性を検証する必要がある場合は、独自のビジネス ステート マシン、プロセス履歴に従ってモデルを抽象化するだけで、線形一貫性検証ツールを直接使用して検証できます。その他の一貫性を検証する必要がある場合は、履歴を通じて対応するテストケースを簡単に記述できます。

実際の使用において、履歴生成や検証において独自のニーズを満たしたい場合は、構造ごとに分割して Jepsen の一部のみを使用したり、独自のフレームワークを構築したりすることができます。たとえば、独自のエラー挿入フレームワークを使用して、自分で履歴を生成し、それを Jepsen の一貫性チェッカーに渡すことができます。または、Jepsen を使用して履歴を生成し、それを読み取って分析するための簡単なスクリプトを作成することもできます。または、同様のフレームワークを直接構築して、豊富な機能やシナリオをより効率的に処理し、使いやすく読みやすいテスト コードをすばやく作成することもできます。

さまざまな分散システムにとって、Jepsen は絶対に必要であり、テストの作成と検証が簡単で、エンジニアリング実装におけるさまざまな問題を最低コストで発見するのに役立ちます。

参考記事:

ジェプセンテスト

https://ata.alibaba-inc.com/articles/109813

メッセージングとジェプセンが出会うとき

https://developer.aliyun.com/article/727886

線形化可能性理論

https://zhuanlan.zhihu.com/p/338057286