Linearizability

code:markdown

- 各操作は一点の瞬間で起きたとみなせる

- 実時間の順序を守る

Linearizabilityの定義

Linearizability（線形化可能性）はatomic consistency（アトミック整合性）とも呼ばれ、Herlihy & Wing (1990) が形式化した分散システムにおける最も強い単一オブジェクトの一貫性モデルである。一言で言えば、システムが単一のレプリカしか存在しないかのように振る舞うことを保証する。

形式的には、以下の2つの条件を同時に満たす実行履歴をlinearizableと呼ぶ。

1. 各操作に「効果が発生した単一の時点」（linearization point）が存在し、それは操作の開始（invocation）から終了（response）までの間のどこかに位置する。つまり操作が瞬時に完了したかのように見える

2. ある操作が完了した後に開始された別の操作は、必ず前の操作の結果を観測する（最新のデータが返る）

この2つの条件は「分散システムが単一ノードであるかのように振る舞う」ことの形式的な表現である。分散データストアのレプリケーション間の一貫性や、共有メモリシステムにおけるオブジェクトへの並行アクセスなど、強固な一貫性が求められる場面で基準となるモデルである。なお、マルチコアCPUの実際のメモリモデル（x86のTSO等）はlinearizabilityより弱く、sequential consistencyに近い保証に留まる。linearizabilityはあくまで理論上の基準点であり、ハードウェアが常にこれを満たしているわけではない。

なぜLinearizabilityが重要か

単一ノードのシステムでは、すべての操作は物理的に直列化される。プログラマが暗黙に期待する「書いたらすぐ読める」「完了した操作の結果は消えない」という感覚は、このモデルに対応している。linearizabilityが成り立つ系ではプログラミングが容易になる。分散の複雑さを意識せず、単一マシンを相手にしているかのようにコードを書ける。

銀行口座の残高が100円のとき、50円を引き落とした直後に残高を確認したら50円が返るべきだ、というのはlinearizabilityそのものである。これより弱い一貫性モデル（例えばsequential consistency）では、引き落とし完了後でも100円が返る可能性が理論上排除できない。

linearizabilityは「直感的な正しさ」と「形式的な定義」が一致する稀有なモデルであり、だからこそ分散システムの正当性を議論する基準点として広く使われている。

Linearizabilityの持つ性質

合成可能性（Composability）

linearizabilityには局所性（locality）と呼ばれる性質がある。個々のオブジェクトがそれぞれlinearizableであれば、それらを組み合わせた系全体もlinearizableになる。

この性質は実用上の利点が大きい。システムの各コンポーネントを独立にlinearizableに設計すれば、全体の正当性が自動的に保証される。モジュラーな設計と相性が良い。

実時間順序の尊重

linearizabilityが他の一貫性モデルと決定的に異なるのは、操作間の実時間的な前後関係を保存する点である。操作Aが完了した後に操作Bが開始された場合、Bは必ずAの結果を観測する。

この制約こそがlinearizabilityを「最も強い単一オブジェクトの一貫性モデル」にしている根拠であり、同時にその実現コストを決定づけている要因でもある。

Linearizabilityの実現コスト

linearizabilityには本質的なコストが伴う。これは実装の問題ではなく、理論的な限界である。

linearizableなread/writeレジスタの実装には、少なくともメッセージの往復遅延に比例するレイテンシが必要であることが証明されている（Attiya & Welch, 1994）。ローカルキャッシュだけで即座に応答を返すことは、linearizabilityの下では原理的に不可能である。

スループットの制約として、グローバルな順序付けは単一のシリアライゼーションポイント（リーダーノードやロック）をボトルネックにしやすい。Raft/Paxosベースのシステムではリーダーダウン時にリーダー再選出が完了するまで書き込みが停止する。

まとめると、linearizabilityのコストはレプリカ間の同期が本質的に要求するものであり、性能（レイテンシ）と可用性が犠牲になりうる。これが、linearizabilityを「必要な箇所にだけ適用する」という設計判断の動機になっている。

一貫性モデルの中でのLinearizabilityの位置

linearizabilityを基準点として、他の一貫性モデルが「何を緩めているか」で整理できる。linearizabilityが同時に要求している2つの性質は以下の通りである。

原子性: 各操作にlinearization pointが存在し、その瞬間に効果が発生したかのように見える

実時間順序の尊重: linearization pointは操作の開始から終了の間に位置し、操作間の実時間的な前後関係が保存される

この2つのうち「どちらを、どの範囲で緩めるか」が、スペクトラムの各段階を特徴づける。

Sequential consistencyは実時間順序の制約だけを取り除く。各プロセス内の操作順序は保存されるが、全体の順序が壁時計の時間と一致する必要はない。

Causal consistencyはさらに、因果関係のない操作間の順序をも放棄する。ネットワーク分断下で達成可能な最も強い一貫性モデルであり（Mahajan et al., 2011）、linearizabilityが分断下で不可能になることを示したCAP定理の裏側からの回答に当たる。

Monotonic readsやread-your-writesは、全体的な順序への要求を手放し、個々のクライアント体験を最低限守る局所的な保証である（「値が巻き戻らない」「自分の書き込みが自分に見える」）。

CAP定理とLinearizability

CAP定理のC（Consistency）はlinearizabilityを指す。Gilbert & Lynch (2002) の証明がlinearizabilityを採用した理由は前述の合成可能性にある。

証明の核心を直感的に述べると、ネットワーク分断が発生した状態で一方の区画でwrite(x, 1)が完了し、他方の区画でread(x)が実行されたとき、linearizabilityが要求する実時間順序との整合を満たすにはwriteの結果がreadに反映されなければならない。しかし分断下ではその伝搬ができない。結果として「応答しない（可用性の放棄）」か「古い値を返す（linearizabilityの放棄）」の二択を迫られる。

ただしこの定理は「linearizabilityを常に諦めるべき」とは言っていない。分断がない通常運用時にはlinearizabilityを維持できるし、分断下でもcausal consistencyまでは達成可能である。「どの操作にlinearizabilityが必要で、どこでより弱い保証に切り替えるか」が設計判断の焦点になる。

実装の実例

linearizabilityを提供するシステムとして、etcdやZooKeeperがある。いずれもRaft/Paxosベースの合意プロトコルによって、リーダーを経由した読み書きのlinearizabilityを実現している。

DynamoDBではstrongly consistent readオプションを選択することで、単一リージョン内でlinearizableな読み取りが可能になる。デフォルトのeventually consistent readとの使い分けは、まさに「操作ごとに一貫性レベルを選ぶ」設計の具体例である。

Cassandraではクォーラム設定（QUORUM/ALL）によってlinearizabilityに近い保証を実現できるが、厳密なlinearizabilityにはLightweight Transaction（Paxosベース）が必要になる。

まとめ

linearizabilityは「分散システムが単一ノードのように振る舞う」ことを形式的に表現したモデルである。直感的な正しさと一致し、合成可能性を持ち、CAP定理の基準点となっている。一方で実時間順序の保証には本質的なレイテンシ・可用性・スループットのコストが伴う。

一貫性モデルの選択とは「linearizabilityから何を緩めるか」を操作単位で判断する行為である。一貫性モデルはシステム全体の属性ではなく操作の属性であり、DynamoDBのConsistentReadフラグやCassandraのクォーラム設定が示すように、同一システム上で操作ごとに異なるレベルを使い分けるのが現実の設計である。linearizabilityを正確に理解することが、その判断の出発点になる。