CALM
CALM (Consistency As Logical Monotonicity) は分散システムの定理 (昔は予想だったけど、証明されたらしい) で、どう分散システムを作ればいいかというもの coordination が要らないような結果整合なプログラム <=> monotonic logic で表すことができる
プログラムを monotonic にすると、coordination レイヤが要らなくなる
non-monotonic な部分は
CALM で調べたら一番上に出てくるスライド
最初のページ見づらいけどあとの方のは大丈夫
CAPでは3つのうち2つしか両立できないということだけど、現実的にはいろいろ工夫できる 障害はそんなに起きない
マシンの数が多くなれば障害自体は頻繁に起こるけど、例えば半分以上が同時に落ちる確率は低い
スケーラブルな分散システムを作るには (注: これは CALM ではない)
一貫性の強さを必要最低限にする
一貫性を保証する部分をクリティカルパスから外したり、滅多に通らない部分にする
mutability はアンチパターン
なぜ？
いまいちわからん
monotonic と non-monotonic がわからん
例が欲しい…
入力に何かを追加しないと出力も増えない
question.icon どういうこと？
CALM は
question.icon の必要なしにってなに？Paxos とか使ってたら強い一貫性あるよね
任意のプログラムで、coordination protocol で単調ではない文 (順序の点) を保護することによって、結果整合性は保証されうる
monotonic
monotonic logic: なんか余計なものが増えても結論は変わらない
P と (P -> Q) があれば Q が成り立つ、P と (P -> Q) と R があれば Q が成り立つ
R がなんか余計だけど、Q が成り立つのは関係ない
R が ~P とかだったらどうするんだろ amutake.icon
これがどう分散システムにつながるのか不明
confluent (合流性)
操作が confluent である := 非決定的な順序の入力の集合が与えられても、同じ出力集合を返す
confluent な操作の合成は confluent である
こういう操作を作るの難しそう amutake.icon
感想 amutake.icon
CAP とか FLP みたいな不可能なことは証明されて広く知られていたりするんだけど、じゃあなにが可能なんじゃ？ってことがよく議論されているようだ こういう原則に則って分散システムを設計するとよさそう
monotonic, confluent, convergent, とかなんかそういうキーワードは他にも出てきそう
参考文献
これの長いコメントがわかりやすいかもしれない
CALM が証明された論文
上の reddit の動画で話している Joseph Hellerstein さんの論文
Keeping CALM についてのまとめ記事
exists のほうが forall よりも簡単って言ってる
例示すればいいので
この例も作為的すぎる気がするけど…