CALM Theorem

• 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://cacm.acm.org/research/keeping-calm/
  • Communications of the ACMの記事
• https://dl.acm.org/doi/10.1145/2450142.2450151
  • 証明した論文
• amutake/CALM