グローバルスナップショット（Chandy-Lamport）

🎓 レベル：発展　|　重要度：B（重要）

📎 前提：論理時計（Lamportタイムスタンプ）　|　関連：ベクトル時計・冪等性と再試行・バックオフ

要点（BLUF）

Chandy-Lamportアルゴリズムは、システムを止めずに「一貫した大域状態（スナップショット）」を記録する古典手法。デッドロック検出・分散GC・チェックポイントに使う。
鍵はマーカー（marker）メッセージ：各プロセスは初マーカー受信時に自状態を記録し、全出力チャネルにマーカーを流す。マーカー以降に届いた実メッセージは「チャネル内（飛行中）」として記録する。
撮れるのは一貫した切断面（consistent cut）：因果を破らない（受信を記録したら対応する送信も記録済み）。どの実時刻にも一致しないかもしれないが、保存量（総額など）は正しく保たれる。

問題設定 ── 全員同時に撮れない

「今この瞬間の全ノードの状態」を撮りたい。だが共通時計が無い（物理時計とクロック同期（NTP））ので「同時」が定義できないし、撮影中にメッセージは飛び続けます。プロセスの状態だけ記録してチャネル内のメッセージを無視すると、保存量が合わなくなります（送金が消えて見える）。

アルゴリズム ── マーカーで切断面を引く

FIFOチャネル（順序保存）を仮定します。

開始プロセス:
  自分の状態を記録 -> 全出力チャネルにマーカー送出
チャネル c でマーカーを「初」受信:
  自分の状態を記録、c を「空」と記録 -> 全出力チャネルにマーカー送出
既に記録済みでチャネル c にマーカー受信:
  c を「状態記録〜マーカー到着の間に届いた実メッセージ列」で確定

sequenceDiagram
    participant A
    participant B
    Note over B: B が A へ 40 送金(チャネル飛行中)
    Note over A: スナップショット開始 -> 状態100を記録
    A->>B: marker
    Note over B: 初marker -> 状態60を記録, A->Bは空
    B->>A: money 40 (先に飛んでいた)
    Note over A: 記録済 -> money40 を B->A の飛行中として記録
    B->>A: marker
    Note over A: B->A を確定

具体例 ── 飛行中の送金を取りこぼさない（実機）

ラボ 02-04_chandy_lamport.py。2口座（合計200が保存量）で、B→Aの送金40がチャネルを飛行中にAがスナップショットを開始：

== 記録された大域スナップショット ==
プロセス状態: {'A': 100, 'B': 60}
チャネル内メッセージ: {('A', 'B'): [], ('B', 'A'): [40]}

プロセス状態合計 = 160
チャネル内(飛行中) = 40
スナップショット総額 = 160 + 40 = 200
不変量(総額200)が保存されている: True

Aは送金40が届く前の状態100を記録し、その40はチャネルB→Aの飛行中メッセージとして別に記録されます。プロセス状態だけ足すと160で合いませんが、チャネル内40を足すとちょうど200。二重計上も取りこぼしもありません。

正しさの観点 ── 一貫した切断面

記録された大域状態は consistent cut（一貫切断面）になります。

安全性：あるメッセージの受信が切断面の「前」に入るなら、その送信も必ず「前」に入る（因果が破れない）。FIFOとマーカーがこれを保証。
保存量の不変性：プロセス状態とチャネル内メッセージを合わせれば、送金のような保存量は厳密に一致する（実証の通り）。
活性：各チャネルにマーカーが1回流れれば必ず終了する。

切断面は「実時刻のある瞬間」とは限りません。Aは100を記録、Bは40を出した後の60を記録——この瞬間は現実には存在しなかったかもしれない。それでも因果的に矛盾しない、というのがポイントです。

なぜ分散だと難しいか（直観）

「同時に撮る」が無理なので、因果的に矛盾しない切断面で妥協する。マーカーは「ここから後のメッセージは切断面の向こう側」という境界線の役割。FIFO仮定により、マーカーより前に送られたものはマーカーより前に届く——この順序保存が切断面の一貫性を支えます。

⚠️ よくある誤解・落とし穴

「スナップショット＝ある瞬間の写真」→ 違う。どの実時刻とも一致しない一貫切断面のことがある。一致するのは保存量。
「プロセス状態だけ記録すればよい」→ チャネル内メッセージを忘れると保存量が壊れる（送金が消える/増える）。
「非FIFOでも動く」→ 素朴版はFIFOチャネル前提。非FIFOでは追加の工夫が要る。
「全プロセスを止めれば簡単」→ 止めると可用性が死ぬ。止めずに撮るのがこの手法の価値。

対応ラボ

distributed-systems-study/labs/02-04_chandy_lamport.py（飛行中送金を含め保存量200が一致することを確認済み）。