## 定義 システムモデルとは、分散アルゴリズムがどのような障害・タイミングの前提のもとで正しく動作すると保証されるかを形式化した抽象である。アルゴリズムはハードウェア・ソフトウェア構成の細部に依存しすぎないよう記述する必要があり、そのために「どのような故障がどの程度の頻度・パターンで起こりうるか」を事前に明示する。(Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") ## タイミングに関する3モデル - **同期モデル(synchronous)**: ネットワーク遅延・プロセス一時停止・クロック誤差のいずれにも有限の上限があると仮定する。現実のシステムのほとんどは非有界な遅延や一時停止が実際に起こるため、現実的なモデルではない。 - **部分同期モデル(partially synchronous)**: ほとんどの場合は同期システムのように振る舞うが、時折その上限を超える。現実の多くのシステムに最も近いモデル。 - **非同期モデル(asynchronous)**: タイミングに関する仮定を一切置かない(クロックすら持たずタイムアウトも使えない)。設計できるアルゴリズムは非常に制限される。 (Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") ## ノード故障に関する4モデル - **クラッシュ停止(crash-stop / fail-stop)**: ノードはクラッシュのみで故障し、故障後は二度と復帰しない。 - **クラッシュ回復(crash-recovery)**: ノードは任意の時点でクラッシュしうるが、不揮発性の安定ストレージの内容を保持したまま未知の時間の後に復帰しうる(インメモリ状態は失われる)。 - **劣化性能・部分機能停止(degraded performance / partial functionality)**: クラッシュせずに極端に遅くなる、あるいは一部の機能だけ停止する。この状態は*limping node*・*グレイ障害*・*fail-slow* とも呼ばれる([[グレイ障害]] 参照)。 - **ビザンチン(恣意的)障害**: ノードが他ノードを騙そうとするなど、任意の振る舞いをしうる([[ビザンチン障害]] 参照)。 現実のシステムをモデル化するには、部分同期モデル + クラッシュ回復モデルの組み合わせが最も有用とされる。(Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") ## 安全性(safety)と活性(liveness) アルゴリズムの正しさは、満たすべき「性質(properties)」の列挙で定義する(例: フェンシングトークンの一意性・単調増加性・可用性)。これらの性質は 2 種類に分類できる。 - **安全性(safety)**: 「悪いことが起きない」性質。違反が起きた瞬間を特定でき、いったん違反すると取り消せない。分散アルゴリズムには、システムモデルが許すあらゆる状況(全ノードのクラッシュ・ネットワーク全断を含む)で常に安全性を要求するのが一般的である。 - **活性(liveness)**: 「良いことがいつか起きる」性質。定義に "eventually"(いつか)という語を含むのが典型的な目印。ある時点で未達成でも将来満たされる望みが残る。活性には「過半数のノードがクラッシュしていない限り」「ネットワークがいずれ回復する限り」といった留保をつけることが許される。結果整合性(eventual consistency)は活性の一例である。 (Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Distinguishing between safety and liveness") ## モデルと現実のギャップ 理論的なシステムモデルは現実の単純化にすぎない。たとえばクラッシュ回復モデルは安定ストレージがクラッシュを生き延びると仮定するが、実際にはディスク破損やファームウェアバグでデータが失われることがある。クォーラムアルゴリズムはノードが自身の保存データを正しく記憶していることに依存するため、この前提が崩れると正しさも崩れる。理論的アルゴリズムは「起こらないと仮定する」ことを宣言できるが、実装は`printf("Sucks to be you"); exit(666);` のように、想定外の事態への対処コードを持たざるを得ない——これは計算機科学と工学の違いの一つである。(Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Mapping system models to the real world") ## 横断的知見 - **Database Internals 第II部序論の非形式的な記述は、DDIA が形式化するタイミングモデル・ノード故障モデルの前段に位置づけられる**: Petrov は第II部序論で「通信チャネルはメッセージを遅延させたり順序を変えたり配信に失敗したりし、プロセスは一時停止・スローダウン・クラッシュ・制御喪失に陥り、応答不能になることもある」と非形式的に述べるにとどまるが、これはまさに DDIA が形式化する同期/部分同期/非同期のタイミングモデルと、クラッシュ停止/クラッシュ回復/劣化性能/ビザンチンというノード故障モデルが対象とする現象そのものである。両者を並べると、実務者向けの入門(Database Internals)がまず現象を列挙し、より理論志向の教科書(DDIA)がそれを性質(安全性・活性)の充足条件として体系化する、という記述の深化の順序が見える。(Source: [[@2021__OReillyJapan__詳説 データベース - Part II 序論 分散システム]], [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") - **本概念は TLA+・軽量形式手法の検証対象そのものを定義する**: [[TLA+]] や [[軽量形式手法]] が検証するのは、まさに本概念の「性質(properties)」——安全性・活性の充足である。DDIA 第9章はフェンシングトークンの一意性・単調増加性(安全性)・可用性(活性)を具体例に挙げるが、[[TLA+]] ページが扱う Azure CosmosDB のインシデント分析ワークフローも「設計がどのような性質を保証するはずだったか」を事後的に明文化する営みであり、本概念の性質定義の枠組みと同型である。[[軽量形式手法]] の ShardStore 事例も、正しさの特性(逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなし)を分解して検証ツールを割り当てる設計であり、これは本概念のクラッシュ回復モデルの精緻化(単一クラッシュ vs 並行クラッシュ)に対応する。(Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Defining the correctness of an algorithm", [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]], [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]) - **[[障害検出器]]の完全性/正確性は、DDIA の活性/安全性の枠組みの具体例として読み替えられる**: [[@2021__OReillyJapan__詳説 データベース - Chapter 9 障害検出]]は、障害検出機能の必要不可欠な特性として「完全性(すべての障害のないメンバーが最終的にプロセスの障害を認識できる)」と「正確性(プロセスの障害が正確に検出される)」を挙げ、これらを明示的に活性・安全性という語で説明する——完全性は「いずれかのプロセスが障害を発生した場合、障害検出機能はその障害を必ず検出しなければならない」という活性の定義そのものであり、正確性は「あるプロセスに dead のマークを付けた場合、そのプロセスは実際に停止していなければならない」という安全性の定義そのものである。DDIA 第9章がフェンシングトークンの一意性・可用性を安全性・活性の抽象例として挙げるのに対し、Database Internals 9 章は障害検出という具体的な機能単位で同じ 2 分類を再現しており、「安全性・活性という性質分類が特定のアルゴリズムに依存しない一般原則である」ことを別ソースから裏付ける。ただし Petrov は "eventually" という語を明示的には使わず「最終的に(まいずれ)認識する」という日本語表現で活性を述べており、DDIA の形式的な語彙とは独立に同じ概念へ到達している点も観察できる。(Source: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Distinguishing between safety and liveness", [[@2021__OReillyJapan__詳説 データベース - Chapter 9 障害検出]] p.202) - **完全性と正確性のトレードオフは、安全性と活性が「対称でない」ことを障害検出という具体例で示す**: 本概念は DDIA 由来で「分散アルゴリズムは安全性を常に要求する一方、活性には留保が許される」という非対称性を記録してきたが、Database Internals 9 章はこれをさらに実務的に肉付けする——「精度と効率性を兼ね備えた障害検出機能を構築することはおそらく不可能」であり、「障害検出機能は偽陽性を生成する、つまり誤って正常なプロセスに障害があると識別するか、あるいはその逆に識別することが許容される」[CHANDRA96]。すなわち障害検出器の実装においては安全性(正確性)そのものすら厳密には達成不可能であることが前提とされており、DDIA が抽象的に述べる安全性優先の原則を、障害検出という具体的なサブシステムでは緩和せざるを得ない実例になっている。(Source: [[@2021__OReillyJapan__詳説 データベース - Chapter 9 障害検出]] p.202, [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Distinguishing between safety and liveness") - **Database Internals 第8章は、第II部序論の非形式的な現象列挙と DDIA の完全な形式化との「中間段階」を占める**: 第II部序論(前章)は「通信は遅延・順序変更・配信失敗しうる」と現象を列挙するにとどまるが、第8章§8.6は同期(タイミングに上限あり)・非同期(タイミング前提なし)・部分同期(ほとんどは同期的だが時折上限を超える)という3モデルを名前付きで導入し、DDIA第9章の3モデル分類とほぼ同一の粒度に達する。同様に第8章§8.7はクラッシュ障害・欠落障害・任意障害(ビザンチン障害)という3分類を導入し、DDIA第9章の4分類(クラッシュ停止・クラッシュ回復・劣化性能・ビザンチン)の前段(クラッシュ障害はクラッシュ停止/クラッシュ回復の両方を包含する形で導入され、劣化性能に相当する明示的な第4カテゴリは第8章にはまだ独立して立てられていない)に位置づけられる。さらに第8章§8.5のFLPの不可能性(→ [[FLPの不可能性]])は、「なぜ非同期モデルでは有界時間内の合意保証が原理的に不可能か」という、本概念のタイミングモデル分類そのものを動機づける不可能性証明を提供しており、DDIA第9章にはこれに相当する定理の直接引用がない。すなわち第8章は現象論(前章)と形式化(DDIA)の間で、名前付きモデルと不可能性証明という2つの理論的支柱を独自に備えた中間層を成す。(Source: [[@2021__OReillyJapan__詳説 データベース - Chapter 8 基本事項の紹介と概要]] §8.5〜§8.7, [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") ## 未解決の問い - Database Internals 第II部の後続章(リーダー選出・レプリケーション・合意)は、本概念のシステムモデル(同期/部分同期/非同期、クラッシュ停止/クラッシュ回復/劣化性能/ビザンチン)のうちどれを暗黙の前提として採用しているか。章を追って明示的に確認する必要がある。9 章「障害検出」はビザンチン障害の不在を明示的に前提としており(「以下で検討するアルゴリズムでは、ビザンチン障害は存在しないことを前提にします」)、クラッシュ停止またはクラッシュ回復モデルのいずれかに限定して議論している。 - [[障害検出器]]が厳密には安全性(正確性)すら達成不可能と明言する一方、本概念は分散アルゴリズム一般について「システムモデルが許すあらゆる状況で常に安全性を要求するのが一般的」と記録してきた。障害検出器はこの原則の例外なのか、それとも「検出器自体の正確性」と「検出器を利用する上位アルゴリズムの安全性」は別レイヤーの安全性であり矛盾しないのか。 - クラッシュ回復モデルの「安定ストレージはクラッシュを生き延びる」という前提が崩れる場合(ディスク破損等)に対応する、より精緻なシステムモデルは実務でどこまで採用されているか。[[軽量形式手法]] の ShardStore はこの種の前提崩壊をどこまで検証範囲に含めているか。 - 安全性と活性の区別は、[[軽量形式手法]] が挙げる「並行クラッシュ実行の検証」という未解決の問いにどう関係するか。並行クラッシュ下での安全性証明は、逐次クラッシュ下の証明とどう技術的に異なるか。 - TLA+ のようなモデル検査ツールで安全性違反を発見するのと、活性違反(いつまでも satisfy されない)を発見するのとでは、検証手法(有界探索・時相論理)にどのような違いが必要か。 - Database Internals 第8章のクラッシュ障害・欠落障害・任意障害という3分類と、DDIA第9章のクラッシュ停止・クラッシュ回復・劣化性能・ビザンチンという4分類の対応関係(特に「欠落障害」と「劣化性能」の異同)は明確でない。第II部の後続章(10〜14章)がどちらの分類語彙を使い続けるかを追跡すると、書籍内での用語の一貫性が見えるはずである。 ## 関連 - ソース: [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] / [[@2021__OReillyJapan__詳説 データベース - Part II 序論 分散システム]] / [[@2021__OReillyJapan__詳説 データベース - Chapter 9 障害検出]] / [[@2021__OReillyJapan__詳説 データベース - Chapter 8 基本事項の紹介と概要]] - 概念: [[分散コンセンサス]] / [[TLA+]] / [[軽量形式手法]] / [[部分故障]] / [[グレイ障害]] / [[ビザンチン障害]] / [[障害検出器]] / [[FLPの不可能性]] ## 出典 - Martin Kleppmann and Chris Riccomini, *Designing Data-Intensive Applications*, 2nd Edition, O'Reilly Media, 2026, Chapter 9, "System Model and Reality", "Formal Methods and Randomized Testing". - Alex Petrov, *詳説 データベース*, オライリー・ジャパン, 2021, 第II部序論, 8 章 §8.5〜§8.7, 9 章.