Keep CALM and CRDT on

概要

• CALM Theoremの記事をCACMに書いたJ. M. Hellersteinらの論文
• VLDB 2022: https://www.vldb.org/pvldb/vol16/p856-power.pdf
  • https://arxiv.org/pdf/2210.12605
• CRDTの保証はデータ更新にのみフォーカスが当てられていて、データのReadは安全ではない
  • Early Readとかがある
  • マージとかはmonotonicだけど、クエリはmonotonicなものとそうでないものが混ざってるのが問題
• CALM TheoremのmonotonicityをCRDTに適用して、安全なクエリモデルを作る

クエリの満たすべき性質

• Safety: Queries should be sequentially consistent, regardless of the replica at which they are evaluated

  • これって別に、Sequential Consistencyとは関係ない…? monotonic readsみたいな話?(kekeho)

• Efficiency: Queries should be evaluated locally without coordination whenever possible

  • whenever possible…(kekeho)

• Simplicity: The query model should be easy for developers to reason about.

• Sequential Consistencyを満たすクエリの例: ローカルレプリカのGrow-only Setに対して、要素数がnを越えているかチェックするクエリ

  • ローカル状態はグローバル状態のサブセット。monotonicだ!

• 満たさないクエリの例: [Potato Ferrari Problem]

  • ローカル状態がグローバル状態と等しいことを保証できない限り、ローカル状態がグローバル状態と等しいとはいえない。non-monotonicなクエリだ!

• Monotone query: a query $Q$ is monotone if $\forall i,j\in D:i\le j,Q(i)\Rightarrow Q(j)$

  • $D$はState-based CRDTの取りうる状態集合
  • 任意の状態i, jについて、iがjよりも小さいならば、クエリ$Q(i)$が真ならば$Q(j)$も真となる
    • CRDTの状態が進むにつれて、クエリの結果は偽から真になることはあっても、真から偽に変わることはない(kekeho)
  • Safety, Efficiency, Simplicityを満たす
  • monotone queryの合成もまた、monotoneである(CALM TheoremでのComposabilityの議論)

• CRDTsでは、Non-MonotonicなQueryのみを順序付けてやればよい