S3の技術的詳細分析
catatsuy1) S3の“外から見える単純さ”と“中の現実”
S3がユーザーに見せている基本操作は極端にシンプルで、会話でも繰り返し「put/getが心臓」と言っています。ところが中では、
- 数百万台規模のサーバ／数千万台規模のドライブ
- 38リージョン・120AZ
- 500兆オブジェクト・数百EB
- 毎秒数億〜数億超のトランザクション（発言上 “hundreds of millions TPS”）
という“常時故障が起きて当たり前”の世界で、しかもユーザーはそれを意識せず「ただ動く」を期待する。
このギャップを埋めるために、S3は データプレーン(put/get)とは別系統の、耐久性・修復・監査の宇宙（多数のマイクロサービス）を常時動かし、故障を「例外」ではなく「前提」として扱っています。
2) 強整合(Strong Consistency)を“ほぼ一夜で”ロールアウトできた理由の分解
会話で出てくる「replicated journal」と「cache coherency protocol（failure allowance付き）」は、強整合の要点を次のように分解して理解するのがよいです。
2.1 どこが難しいか：強整合の“敵”
強整合の敵は単に「ノードが落ちる」ではなく、
- キャッシュが多段に存在する
- 多数のフロント／バックエンドが並列にリクエストを受ける
- 部分故障（あるAZ、あるラック、ある電源系）
- 同時多発（correlated failure）
- 復旧途中・クラッシュ途中の中間状態（crash consistency）
です。強整合は「最新のputが必ず見える」だけでなく、クラッシュや復旧やキャッシュの並行性を含む全状態空間で破綻しない必要があります。
2.2 replicated journal：順序の“背骨”を作る
会話で説明されている replicated journal は、直感的には
- 書き込みが ノード列を順番に流れる
- 各ノードが (value, sequence number) を学習
- 読み出し（特にキャッシュ経由）でも sequence number を使って整合性判定
という「順序(シーケンス)をシステム全体に配る」仕組みとして語られています。
強整合の核心は「最新版とは何か」を合意できることなので、この“順序の背骨”がまず要る。
2.3 cache coherency + failure allowance：可用性を落とさず“複数受付”する
順序だけだと、単一点やボトルネック、あるいは故障時の待ちで可用性が落ちます。そこで cache coherency protocol に failure allowance を入れ、
- 複数サーバが同時にリクエストを受けてよい
- ただし 一定の故障や遅延を許容しつつも、整合性が破れない
という設計をとっている、という説明になっています。
要は「強整合＝単一路線」ではなく、整合性の根拠（順序）と、並列受付（可用性）を両立させるためのキャッシュ整合がセット。
2.4 “コストは増えるが価格に転嫁しない”の含意
彼女は「ハードウェアコストがある」と明言しつつ、顧客課金に載せなかったと言っています。これは“気合い”というより、S3のプロダクト哲学（ビルディングブロック化、ユーザーがコストを意識せず使える）と整合します。
3) 「正しさ(Correctness)」をどう“知る”か：形式手法が“運用の一部”になる瞬間
会話では「強整合を“言う”だけでなく“知る”必要がある」と言い、そのために automated reasoning / formal methods を日常運用に組み込んだ、と説明されています。
ここを、アップロード論文（ShardStore）で具体化すると、「S3は形式手法を“証明書作成イベント”ではなく、継続的に回る検査機構として使う」方向に寄せています。
4) 論文(ShardStore)が示す“現実的な形式手法”の中身（ここが一番具体的）
論文が扱うShardStoreは、S3のストレージノード（キー・バリュー）で、既存S3内に段階的ロールアウトされ、Rustで4万行超、すでに数百PBを保持している、という立ち位置です。
そして「完全検証は現実的でないので、軽量(lightweight) で自動化でき、非専門家でも回せる方法に寄せた」と明言しています。
4.1 ShardStoreが“難しくなる要因”のセット
ShardStoreは性能のために、以下を組み合わせます（＝正しさが壊れやすい温床）：
- soft-updates系のクラッシュ一貫性プロトコル
- 広範な並行性
- append-only I/O
- GC（reclamation / compaction）
-
多様なストレージメディアへの対応
…という“実用システムの全部載せ”。
ここが重要で、強整合の話（replicated journal 等）とはレイヤが違うものの、**「常時故障」「バックグラウンド保守」「並行性」「クラッシュ後も整合」**という同じ性質を、今度は“ストレージノード内部”の具体実装として叩いています。
4.2 彼らの結論：3要素で“日常に落とす”
論文のアプローチは大きく3つ（論文本文でこの流れを説明しています）。まず 参照モデル(reference model)を“実行可能”にする方針が核です。
（＝仕様を紙で書いて終わりにせず、テストで突き合わせられる“動く仕様”にする）
その上で、対象の性質を段階分割して叩きます。
(A) 逐次（単一スレッド）機能正しさ：参照モデルとの“適合(conformance)”
APIの意味論を参照モデルで定義し、プロパティベーステストで多様な履歴を生成して突き合わせる、という構図。
(B) クラッシュ一貫性：Dependency（永続化依存）をテスト可能な形にする
論文が面白いのは、クラッシュ一貫性を「すべてのブロック落ち方を全探索」ではなく、Dependencyオブジェクト（この操作が永続化されたかどうかを問い合わせられる）を軸に検査する設計にしている点です。
-
テストの操作集合に DirtyReboot(RebootType) を追加し、クラッシュ時にどの揮発データがフラッシュされるかを変える
-
再起動・リカバリ後、各ミューテーションが返したDependencyについて
- “永続化されたなら、読み出しは参照モデルと一致する”を検査する
- clean reboot では “最終的に永続化される(前進性)” も確認する
さらに、粒度が粗い（コンポーネント単位でflushする）弱点は認めつつ、flush操作を履歴に挿入して部分フラッシュ状態を作ることでバグ発見確率を上げています。
ブロックレベル全列挙版も実装したが遅すぎ、追加バグも出なかったのでデフォルトでは使わない、と現実的判断も書いています。
この設計思想は、会話側の「スケールでは数学が必要」「全組合せは無理」発言と同型で、**“網羅”ではなく“継続・自動・局所化された強いチェック”**へ寄せています。
(C) 並行性：線形化可能性を狙うが、スケール限界を踏まえツールを使い分ける
理想は「参照モデルに対するlinearizability」だが、現実には重い。そこで、
- Rust向け stateless model checker Loom：小さいが重要な並行コードを全インタリーブ探索（release/acquireモデルでCDSChecker系、PORで爆発緩和）
- 大きいテスト（end-to-end）はLoomがスケールしないので、彼らは Shuttle を開発・OSS化し、確率的/ランダム化アルゴリズムで大規模並行テストを回す（健全性 vs スケールのトレードオフ）。
さらに、具体例として compaction と reclamation の競合で“参照されていない新チャンクが回収され、メタデータが後からそのチャンクを指してダングリングになる”という、いかにも現場で踏みそうなレースを示し、対策として「書き込み先extentをロックしてメタデータ更新まで保護」したと書きます。
これ、会話側の「correlated failureが怖い」「クラッシュ一貫性を深く考える」と同じく、バックグラウンド作業が“主処理の不変条件”を壊す典型です。
4.3 “その他の正しさ”まで手が届く：unsafe/シリアライゼーション
ShardStoreはRustでもunsafeが避けられず、未定義動作を潰すため Miri でテストを回し、必要な並行プリミティブ対応をRust本体へupstreamした、とあります。
また、ディスク上データはビット腐敗や一時故障で壊れ得るので、デシリアライズを“信用しない”前提で扱う姿勢も示しています。
5) Durability（11ナイン）を“測っている”の意味
会話での「auditor microservices が全バイトを継続検査し、修復が自動で走る」「今週/月/年の実測durabilityを答えられる」は、単なる監視ではなく、
- “永続化の現実”を継続検証するデータパイプライン
- 検知→修復が別系統に自動化
- 故障率モデルの仮定だけに依存しない
という運用設計だと読めます。
形式手法が“仕様・実装の正しさ”を担保し、auditor/repairが“現物データの正しさ（劣化・腐敗・部品死）”を担保する、という役割分担が見えます。
6) correlated failure / crash consistency / failure allowance：3つは同じ話の別投影
会話の重要点を整理すると：
- correlated failure：独立故障は織り込み済み。怖いのは「同じフォルトドメインに束ねられた同時故障」
- crash consistency：停止・部分書き込み・復旧途中など、“中間状態”から常に整合へ戻る設計
- failure allowance：可用性を落とさずに並列処理するため、許容できる故障や遅延の“枠”を設計し、メトリクスでサイズする
論文側のShardStoreの話は、まさに「crash consistency + 並行GC/compaction + append-only」を扱っており、会話の概念が“実装ディテール”に落ちているのが分かります。
7) S3 Tables と S3 Vectors：データレイク→“データオーシャン”の次の足場
7.1 S3 Tables
会話のポイントは「Parquet(+Iceberg)が顧客側で爆発した結果、S3が“テーブルの運用”をネイティブ化した」という流れです。
Icebergを“共通土台”にすると、分析エンジンを取り替えてもデータレイクの互換性を維持できる（分散組織でも統治しやすい）という説明でした。
また「SQLがデータのlingua franca」「LLMがSQLで訓練されている」という話から、S3 Tablesは“開発者がS3 APIを知らなくてもデータに触れる面”を広げる意図が読み取れます（ただし実際のSQL実行系の詳細はこの書き起こし範囲では踏み込んでいません）。
7.2 S3 Vectors：完全に新しいプリミティブ
S3 Tablesが「オブジェクト(Parquet)を管理してテーブル化」なのに対し、Vectorsは「オブジェクト上に載せた抽象」ではなく、新しいデータ構造と明言されています。
会話のアルゴリズム的要点は近似最近傍探索(ANN)をどう“ディスク中心”で低遅延にするかで、
- vector neighborhoods をオフライン非同期で事前計算（クラスタ）
- 挿入時にベクタを1つ以上のneighborhoodに配置
- クエリ時は「近いneighborhoodをまず探し」、該当部分だけを高速メモリにロードして最近傍計算
- “warm”でサブ100msを狙う、という説明
です。
ここは典型的な「全比較は高コスト→候補集合を前処理で絞る」戦略で、S3流に“スケールを味方にする”（事前計算と分散・キャッシュ）へ寄せています。
8) 最後に：この回の“設計哲学”を一言でいうなら
このエピソードと論文を合わせて見ると、S3がやっているのは一貫して：
- 故障は例外ではなく常態
- 正しさは主張ではなく、継続的に“検査可能な形”に落とす
- 網羅的完全証明ではなく、参照モデル・プロパティベース・モデルチェックを組み合わせて“毎日回る”仕組みにする
- スケールで悪化する設計を禁止し、スケールで“むしろ有利になる”形に作る
ということです。