- [https://cacm.acm.org/research/keeping-calm/](https://cacm.acm.org/research/keeping-calm/) - CALM: Consistency As Logical Monotonicity # 概要 - [[Program Consisitency]]: [[Consistency]]の定義を、操作の順序づけから決定論的なプログラムの結果にシフトする考え方？ - 既存の[[Consistency]]の議論([[Linearizability]]など)では、メモリアクセスの順序を制約することで一貫性を担保していた - このモデルでは、特定のプログラムの結果の一貫性に、Coordinationが必要かどうかの議論を曖昧にしていた - どのようなProblemであっても、Coordinationを必要としない解があるのか、それとも必要なのかをどうやって知ることができるのか? - アナロジー: 交差点問題。一時停止の信号をどう制御するかに腐心しなくても、片方の道にトンネルを掘れば信号自体をなくすことができる - [[Coordination-free]]なComputational Problem: Coordinationを使わずに一貫性のある出力を計算することができる分散実装が存在するComputational problem - どのような問題群はCoordination-freeなのか? そしてどのような問題群はその外に位置するのか? - Coordination-freeな例: Distributed [[Deadlock detection]]では、[[Wait-for graph]]の全体が見えていなくても部分グラフにサイクルを見つけた時点でそこでデッドロックが発生していることがわかる - Coordination-freeでない例: [[Distributed GC]]では、Rootからの参照グラフ全体が見えないとObjectの参照が一切ないことがわからないので、捨てられない。グラフ全体を知るためにCoordinationが必要 - Def 1. A problem P is [monotonic if for any input sets $S$, $T$ where $S \subseteq T$, $P(S) \subseteq P(T)$] - Distributed [[Deadlock detection]]は部分グラフのInputとOutputは全体グラフのInput/Outputに含まれる - [[Phantom deadlock]]もあるが、ここでは別にその存在について議論しているわけではない(kekeho) - Theorem 1. Consistency As Logical Monotonicity (CALM): A problem has a consistent, corrdination-free distributed implementation if and only if it is monotonic - monotonicである場合、かつその場合に限り、問題は一貫性のある、Coordination-freeな分散実装を持つ - 直感的には、monotonicな問題は、情報(Input)が欠落していても安全であり、協調無しで進めることができる。逆に非monotonicな問題は、新しい情報(Input)に直面したときにある性質の真理が変化することを懸念しなければならない。したがって、すべての情報が到着したことを知るまで先に進めない - monotonicな問題は、inputの到着順序に依存しない。non-monotonicな問題は、入力の順序で出力が変わる - [[Relational transducer]]: 形式的な分散計算モデル - 分散計算可能性の証明には、何らかの形式的な分散計算モデルが必要なので、amelootらは[[Relational transducer]]を用いた - 操作: Relational transducerは、イベントループで以下の操作を順番に実行する - Ingest and apply: 順序付けされていないリクエスト(レコード挿入・削除)のバッチを読み込んで、適用する - Query: ローカルの[[Relation]](レコードの集合)をクエリして、計算処理を行う - 非単調性をもたらすような[[Universal quantifier]]$\forall$, [[Negation-centric equivalent]]$\neg\exists$は使わない - 例えば、$\neg\exists x : P(x)$というクエリが一時的に真でも、あとから追加で$P(x)$を満たす$x$がやってきて、偽になるかもしれない。これはmonotonicityを満たさない(kekeho) - Send: クエリの結果をローカル・他マシンに送る - Theorem 1のifの証明の概要: monotonicな[[Relational transducer]]のネットワークでは、最終的に決定論的な入力を得て、決定論的な出力を生成する。また、実行中の任意の時点において、$P(S) \subseteq T(S)$。 - only ifの証明: - メッセージを、Relational transducerのデータフローメッセージと、他の[[Coordination]]に使うメッセージを分けて議論を進める。 - 仮にデータが1箇所にすべて集められているとして、それでも送られるデータってのはCoordination message。だって明らかにデータフロー以外の目的(=[[Coordination]])に使われているから(kekeho) - うーんそうっすけど、でもほんとに? 納得感があまりない(kekeho) - 非単調操作が常にCoordination messageを送る必要があることを証明する - ここ具体的にどう証明するんだろう。証明した論文を読まねば(kekeho) # メモ - CALMは、[[CAP定理]]のC,A,Pが同時に満たせる問題のクラスを規定する - [[Coordination free]]であることは、[[Network partition]]下での[[Availability]]と等価 - [[Coordination free]]ということは、[[Network partition]]下でも独立で処理を進められる - パーティションから回復するとき、状態のマージはmonotonicであり、一貫している - たしかに!(kekeho) - Cが、CAPは[[Linearizability]]だったが、CALMでは[[Program Consisitency]]の[[Confluence]] - うーん、やっぱりCが違うから比べて良いのかな?(kekeho) - Monotonic Problemは、協調が必要ないだけでなく、ネットワーク[[メンバーシップ]]の知識を必要としない問題でもある - 確かに、データフローは[[Gossip Protocol]]等で十分だよな(kekeho) ## うんちく - [[PODS]] 2010で予想が発表されて、amelootらが色々形式化とか証明とかをした - [[Bloom言語]]で活用されている? # 参考資料 - [https://speakerdeck.com/jhellerstein/the-calm-theorem-positive-directions-for-distributed-computing](https://speakerdeck.com/jhellerstein/the-calm-theorem-positive-directions-for-distributed-computing) - [https://cacm.acm.org/research/keeping-calm/](https://cacm.acm.org/research/keeping-calm/) - Communications of the ACMの記事 - [https://dl.acm.org/doi/10.1145/2450142.2450151](https://dl.acm.org/doi/10.1145/2450142.2450151) - 証明した論文 - [amutake/CALM](https://scrapbox.io/amutake/CALM)