#分散システム
厳密な検証からデバッグ用途程度のものまで適当に入れてる
定理証明 (theorem proving)
仕様を演繹的に証明
Verdi
分散システムとは
例によって人によって定義がいろいろある気がする
複数のマシンがネットワークを介して繋がれている
一部が死んでも全体ではシステムとしての機能は保つ、あるいは変な状態にならない
一部というのがどの範囲か: 故障モデル
分散システムがどの程度激しく故障するか。ある分散アルゴリズムについて、「この故障モデルならこの性質は満たされるけどこの故障モデルでは満たされない」みたいに使ったりする。
Byzantine failure, Arbitrary failure
なんでもありの最強の故障モデル
bitcoin とかはこのモデルだと思う
Authentification detectable byzantine failures
amutake
コード
https://github.com/amutake
技術的興味
分散システム
分散システムを正しく書くのは難しい
可読性が高い・テストしやすいといったコードを書くにはどういった言語機能があればいいのか考えたい
難しいところ
Erlang だと、
メッセージがネットワークを越えるかわからない
分散システムのモデル
非同期分散システム
各プロセスが非同期に動く
同期分散システム
すべてのプロセスが同期して1ステップずつ実行される
#論文
分散システム系
『Linearizability: A Correctness Condition for Concurrent Objects』
Linearizability の元論文
『A comprehensive study of Convergent and Commutative Replicated Data Types』
#書籍
『Fault-Tolerant Agreement in Synchronous Message-Passing Systems』
DAMPS の Raynal 先生の本
https://kuenishi.hatenadiary.jp/entry/2014/09/22/225133 でおすすめされている
分散システムでメッセージをブロードキャストするレイヤ
どのくらいまで保証してくれるかはいろいろある
Best-effort broadcast
pip_ipi と pjp_jpj が正常なら pip_ipi からブロードキャストされたメッセージが pjp_jpj にいつか届く (配送される)
同じメッセージが2回以上届く (配送される) ことはない
分散システムでよくでてくるトピック。
雑多に用語だけ挙げてく
consensus
replication
一貫性モデル、いろいろあってよくわからん問題
Atomic Consistency, linearizability, 線形化可能性
操作が実時間上のどこか (かつその操作の時間内) にプロットされて直列になる
操作の事前条件と事後条件が直列につながる、だと思う
CALM (Consistency As Logical Monotonicity) は分散システムの定理 (昔は予想だったけど、証明されたらしい) で、どう分散システムを作ればいいかというもの
coordination が要らないような結果整合なプログラム <=> monotonic logic で表すことができる
https://www.reddit.com/r/programming/comments/1kmrd3/the_calm_conjecture_has_been_proven_and_is_now/cbqr9ac/
#分散システム #P2P #pubsub
amutake が作ったメディアストリーム中継システム
ひとつのストリームを多数のノードに効率的かつ弾力的 (resilience) に送り届けるシステム
効率的: メッセージ送信の回数。経路が構築されて安定すれば、ノード数Nに対してメッセージ送信もNになる
メッセージIDだけ他にも伝えるとかはあるけど
POPL'14 の論文
CRDTs を引用している文献リストを見ていて見つけた
概要
地理分散システムは可用性とパフォーマンスを得るために複製された結果整合なデータストアをよく使うよね
更新の衝突を解決するために、複製データ型 (replicated data types) と呼ばれる一貫なプロトコルを提案したよ
#論文 #分散システム #churn
churn: ノードの参加・離脱・故障などによってノードの集合が変わること
churn が起きまくるとパフォーマンスに影響が出たり安定性が下がる
どうやったら churn を最小にできるか
#論文 #分散システム
Abstract
Eventual consistency は、同期機構なしで、レプリカの状態が収束するという保証を目的とする
既存の eventual consistency に関する手法はアドホックで間違いが起きやすいものだった
原理的な手法を研究した: eventual consistency を保証するのに十分なシンプルで形式的な条件の上で、データ型の設計方法
linearizability, 線形化可能性 のオリジナルの論文
Herlihy さんが著者
定義 (形式的なの書いてないけど)
history
英語だと linearizability
https://en.wikipedia.org/wiki/Linearizability
元論文: https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf
Herlihyさんが導入した言葉らしい。
#分散システム #論文 #未読
TOCS'2015 (ACM Transactions on Computer Systems)
https://dl.acm.org/citation.cfm?id=2806887
Raft を引用している論文リストを眺めていて見つけた