dshimizu/blog/alpha

とりとめのないITブログ

S3 の論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" に目を通した際の要約・メモ

WIP

はじめに

S3 の論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" に目を通したので内容を箇条書きでメモしていきます。 まだ 「Introduction」までしか見てないので随時記載していきます。

メモ

## Abstract

この論文では、クラウドオブジェクトストレージサービスであるAmazon S3のKey/Value ストレージノード実装である ShardStore の正確性を検証するために、「軽量の形式的手法」を適用した経験が書かれている

* 「軽量の形式的手法」とは、フルタイムのエンジニアリングチームによって継続的な機能開発が行われている運用ストレージノードの正確性を検証するための実用的なアプローチのこと
    * 完全な形式的検証を達成することを目指しているのではなく自動化と使いやすさを重視しており, ソフトウェアとその仕様の両方が時間の経過とともに進化しても 正確さを継続的に保証する
    * 正確さを独立したプロパティに分解し, それぞれが最も適切なツールによってチェックされる仕様として実行可能な参照モデルを開発する形とした
    * 微妙なクラッシュの一貫性や同時実行の問題を含む 16 の問題が本番環境にリリースされるのを防ぎ, ShardStore の進化に伴って新しい機能やプロパティをチェックするために専門家以外の人にも扱えるように拡張された

## 1 Introduction

* S3 について
    * S3 の中核となるのは、オブジェクトデータをハードディスク上に保持するストレージノードサーバーである.
    * これらのストレージノードは、オブジェクトデータのシャードを保持するKVSであり、耐久性を確保するためにコントロールプレーンによって複数のノードにわたって複製されている.
    * S3 は、ShardStore と呼ばれる新しいKVSストレージノードを構築しており、現在のサービス内に段階的にデプロイされている


* ShardStoreのような複雑なシステムに対しての軽量な形式手法
    * ShardStore のようなストレージシステムは正しく理解することが難しい
        * 高い性能を発揮するために, 以下のような仕組みを組み合わせて多様なストレージメディアやその他の複雑な要素をサポートしている
            * ソフトウェアアップデートのクラッシュ整合性プロトコル
            * 高い並行性
            * 追記のみの IO
            * ガベージコレクション
    * 現在の実装はその複雑さを反映して4万行の Rust コードから構成されており, 実装は頻繁に変わり仕様は固定されたものではない. 
        * 変更が世界中に継続的に展開されているエンジニアのチームによって開発および運用されており, 現在、段階的な展開の一環として数百ペタバイトの顧客データを保存している.
    * ShardStore の正確性を検証するためにプロパティベースのテスト, ステートレス モデル チェックなどの軽量の形式的手法のような軽量な形式手法を適用した経験が論文に記載されている
        * 形式手法の専門家以外が自分たちで新機能を検証するための, 自動化された使いやすい軽量な形式手法を探し、形式的な手法を日常のエンジニアリング実践に主流化することが目標
            * 正式な手法を模索したのは、API レベル呼び出しの機能的正確性、ディスク上のデータ構造のクラッシュ一貫性、および同時実行性など、実装の詳細な特性を検証したかったため
        * 軽量で適用が簡単であることと引き換えに, 完全な正式な検証ではなくある程度の正確性の保証を受け入れた.
    * 私たちは3つの要素からなるアプローチに落ち着いた, 要約すると、この論文は主に3つについて貢献している。
        * 頻繁な変更や新機能に直面して、本番規模のストレージシステムの仕様の記述および検証するための軽量なアプローチ。
        * ストレージシステムの正しさを分解し、各特性のチェックにベストな形式手法ツールのスイートを適用する。
        * 軽量の形式手法をプロダクションのエンジニアリングチームの実践に統合し、形式手法の専門家ではなく、彼ら自身が維持する検証アーティファクトを引き継いだ経験。


## 2 シャードストア

* ShardStore
    * ShardStore は、現在 Amazon S3 サービス内にデプロイされている KVS で、複数の HDD を備えたストレージホスト上で実行されている
    * ShardStore KVS は、S3 によってストレージノードとして使用される
    * 各ストレージノードは顧客オブジェクトのシャードを格納し、耐久性を確保するために複数のノードにレプリケートされるため、ストレージ ノードは格納データを内部的にレプリケートする必要がない
    * ShardStore は既存のストレージ ノード ソフトウェアと API 互換性があるため、リクエストは ShardStore または既存の Key-Value ストアのいずれかで処理できます。
    * このセクションでは、ShardStore の設計とそのクラッシュ整合性プロトコルの背景について説明されている

* 2.1 設計の概要
    * ShardStore は、S3 内の他のシステムに対して KVS インターフェイスを提供している
        * キーはシャード識別子、値は顧客オブジェクトデータのシャード
        * 顧客のリクエストは、S3 のメタデータサブシステムによってシャード識別子にマッピングされている
        * ShardStore のキーと値のストアは LSM-Tree で構成され、Wisc-Keyと同様に、書き込み増幅を減らすためにシャードデータがツリーの外側に保存される
    * LSM ツリーがオブジェクト データをディスクに格納する方法の概要を示した図と内容が表記されている (図は略)
    * ShardStore は、すべてのシャードデータをディスク上の単一の共有ログに集中させるのではなく、エクステント全体にシャードデータを分散する
        * このアプローチにより、各シャードのデータをディスク上に配置して、予想される熱とアクセスパターンを最適化する (たとえば、シークレイテンシーを最小限に抑えるなど) ことが柔軟に可能になる
        * ただし、セクション 2.2 「Crash Consistency」 で説明されているように、ログが 1 つもないため、クラッシュの一貫性がより複雑になる
    * その他、chank の保存と再利用、ディスクとのやりとりのための RPC インタフェース、書き込みシステムコールへのエクステント追加の独自実装について記載されている

参考