# 書誌情報
- **タイトル**: Consistency, Availability, and Convergence
- **著者**: [[Prince Mahajan]], [[Lorenzo Alvisi]], [[Mike Dahlin]]
- **出版年**: 2013
- **ジャーナル・カンファレンス**:
- **Abstract**:
We examine the limits of consistency in fault-tolerant distributed storage systems. In particular, we identify fundamental tradeoffs among properties of consistency, availability, and convergence, and we close the gap between what is known to be impossible (i.e. CAP) and known systems that are highly-available but that provide weaker consistency such as causal. Specifically, in the asynchronous model with omission-failures and unreliable networks, we show the following tight bound: No consistency stronger than Real Time Causal Consistency (RTC) can be provided in an always-available, one-way convergent system and RTC can be provided in an always-available, one-way convergent system. In the asynchronous, Byzantine-failure model, we show that it is impossible to implement many of the recently introduced fork-based consistency semantics without sacrificing either availability or convergence; notably, proposed systems allow Byzantine nodes to permanently partition correct nodes from one another. To address this limitation, we introduce bounded fork join causal semantics that extends causal consistency to Byzantine environments while retaining availability and convergence.
# 概要
- [[CAC Tradeoff]]について説明している論文
- [[Asynchronous System]], [[Omission fault]], [[Unreliable Network]]の環境において、以下のタイトな境界(tight bound)があることを明らかにした
- [[Real Time Causal Consistency]]よりも強い一貫性は、[[Always Available]], [[One-way Convergent]]を達成できない
- [[Real Time Causal Consistency]]は[[Always Available]], [[One-way Convergent]]を達成できる一番強い一貫性(?)
- また、[[Byzantine failure]]の起きうるシステムでは、以下のLower boundがあることが示された
- [[Always Available]], [[One-way Convergent]]システムにおいて、[[Fork Causal Consistency]]やそれより強い一貫性を実現することはできない
- 提案されている[[Fork consistency]]を保証するプロトコルは、分岐後お互いが交わらないことは保証するが、[[One-way Convergent]]は達成しないことに注意
# 2. Consistency, Availability and Convergence([[CAC Tradeoff]])
**システムモデルの仮定**
- [[Asynchronous System]]
- [[Unreliable Network]]
- メッセージは任意(ただし有限)の時間だけ遅延する、リオーダーが起きうるdropされることがある
- 各ノードのメモリはclassical。readによってステートは変わらない(量子コンピュータのメモリモデルとは違う)
- 実装は、操作を順序付け、書き込まれる値を透過的に扱い、読み取りの際には何らかの書き込み操作によって書き込まれた値を読み取る(←[[Integrity]], [[Validity]]のあるシステム?)
## 2.1 Consistency
- [[Consistency]]は[[execution]]に対するテスト。execution $e$がConsistency $C$に対するテストに成功したとき、$e$は$C$-Consistentという
- executionは、ノードの集合とread/write operationsのシーケンスから構成される
- write operation: `Write = (nodeId, objId, value, startTime, endTime)`
- read operation: `Read = (nodeId, objId, writeList, startTime, endTime)`
- `writeList`: readの結果を生成するwrite oprationのリスト。書き込み競合等の理由でreadが複数の結果を返すこともあるためリストになってる。
- こういう定義をすることで、一貫性の問題と競合解決の問題を分離し、前者にフォーカスを当ててる
- `startTime`, `endTime`はoperationの開始/終了の実時間
- Consistencyの強弱
- Consistency $C_s$が$C_w$よりも強い $\iff$ $C_s$で受け入れられるexecutionが$C_w$で受け入れられるexecutionのサブセット($E_{C_s} \subset E_{C_w}$)
- 常にサブセットにならないなら、比較不能
- [[Causal Consistency]]
- [[happened-before]]グラフとよばれる[[DAG]] $G$を考える
- 頂点: execution $e$に含まれるread or writeのoperation、辺: 各頂点間に[[半順序関係]]$\prec_G$を与える
- 以下の整合性チェックを満たすような辺があれば、Causal Consistencyチェックをパスする
- **CC1: 各ノードでの直列順序**:
$v, v'$が任意の同じノードで発生した頂点であるとき、$v.startTime < v'.startTime \iff v \prec_{G} v'$
- **CC2: readは直前のwriteの同時書き込みたちを返す**:
オブジェクト$objId$の読み出し操作に対応する任意の頂点$r$に対し、$r$のwriteList $r.wl$は以下を満たす
$w \in r.wl \iff (w \prec_G r \land w.objId = r.objId) \land (\nexists w': (w \prec_{G} w' \prec_G r \land w'.objId = r.objId))$
- つまり, CC1, CC2で[[happened-before]] relationship、[[Causality]]を表現している
- [[Real Time Causal Consistency]]
- [[Causal Consistency]](CC1, CC2)に加え、以下を満たすのがReal-time-causal consistency
- CC3: 時間が逆行しない
$u, v$を$G$の頂点としたとき、$\forall u, v: u.endTime < v.startTime \rightarrow v \nprec_G u$
(操作$u$のあとに$v$がはじまったとき、$v$ happend-before $u$となることがない)
- 対偶を取ると、$v \prec_G u$なら、$v$の終了後に$u$が始まっている(kekeho)
- とても当たり前のように聞こえるけど、Lamport clock使うだけではこれは満たされない。Vector clock使えば満たせるけど、例えば並行なやつはノードIDで順序付け!wとかやり始めたら満たされなくなる(kekeho)
## 2.2 Availability
- どのようなワークロードでも、どのメッセージが失われ、どのノードが通信できるかに関係なく、全ての読み書きが完了できる場合、Always Availableという