分散スナップショットとChandy-Lamportアルゴリズム

「全体の状態」を撮るのがなぜ難しいか

1台のプロセスなら、ある瞬間にメモリをダンプすればそれが状態です。ところが分散システムには全ノード共通の「今この瞬間」がありません。各サーバーの物理時計はずれており、状態を問い合わせるメッセージ自体が遅延します。ノード A の状態を聞いた直後に A が B へ送金メッセージを出し、その後で B の状態を聞けば、送金が「どこにも存在しない」スナップショットが出来上がります。逆順ならお金が二重に存在します。

ここで欲しいのは厳密な同時刻ではなく、一貫したグローバル状態 (consistent global snapshot) です。定義はこうです。あるイベント（メッセージ受信など）がスナップショットに含まれるなら、それより因果的に前のイベントもすべて含まれていること。送金の「受信」が記録されたのに「送信」が記録されていない、という因果の逆転を許さない切り口、と言い換えられます。

カット（cut）と一貫性

各ノードのイベント列に1点ずつ「ここまでを撮った」という線を引く——これをカットと呼びます。カットが一貫している (consistent cut) とは、カットの左側で受信されたメッセージは、その送信もカットの左側にあること。送信が右（カット後）なのに受信が左（カット前）にある、いわゆる「未来から来たメッセージ」を含むカットは不一貫です。

時間 →
P1: ──●send(m)──────────|cut1     送信はcut後 ─┐
P2: ──────────●recv(m)──|cut1     受信はcut前 ─┘ → 不一貫(因果逆転)

P1: ──●send(m)──|cut2             送信がcut前 ─┐
P2: ──────────●recv(m)|cut2       受信もcut前 ─┘ → 一貫

一貫したカットが捉える状態は、実際に起きたとは限らない点に注意します。並行（因果順序のない）なイベントの相対順序は入れ替え可能なので、撮れた状態は「実際の実行を、起きうる別の正しい実行に並べ替えたときに現れる状態」です。重要なのは、それでも到達可能で矛盾のない状態であり、安定述語の判定には十分だということです。

Chandy-Lamportアルゴリズム

K. Mani Chandy と Leslie Lamport が1985年に示したのが、システムを止めずに一貫したカットを得る手順です。前提は2つ——通信路は信頼でき（メッセージは欠落しない）、かつFIFO（送った順に届く）であること。鍵はマーカー (marker) という、通常のメッセージとは区別できる特別な印を流すことです。

開始ノードはまず自分のローカル状態を記録し、全出力通信路にマーカーを送出します。各ノードは次の規則だけに従います。

直感はこうです。マーカーは「この後ろに送ったものは新しい状態」という境界線として通信路を流れます。FIFO なので、ある通信路で「ローカル状態を記録した後・マーカーが来る前」に受け取った通常メッセージは、まさにカットを跨いで飛んでいた途中のメッセージです。これを通信路状態として捕まえれば、ノード状態＋通信路状態の合計が辻褄の合う1枚になります。

マーカー処理（FIFO通信路を仮定）
on receive MARKER from channel c:
  if 自ノード未記録:
      record local state           # 自分のスナップショット
      record c as empty            # cの途中メッセージは無し
      send MARKER to all out channels
  else:
      record c の状態 =
          「local記録後〜このMARKER到着前」にcで受けた通常メッセージ列

各ノードが「全入力通信路からマーカーを受け取った」時点で、そのノードの記録は完了です。全ノードが完了すれば、断片を集めてグローバルスナップショットが完成します。

何が保証され、何が保証されないか

得られるカットが一貫していることは証明できます。直感的には、あるノードが状態を記録するのはマーカーを受けてからであり、マーカーは送信側の記録後に出されます。よって「受信が記録済み（カット前）なら、その送信も記録済み」が成り立ち、因果逆転が起きません。一方で前述のとおり、撮れた状態は実時刻の特定の瞬間と一致するとは限りません。

この性質が役立つのは安定述語 (stable predicate) の検出です。一度真になれば二度と偽に戻らない性質——たとえばデッドロックや計算の終了——は、一貫スナップショット上で真と判定されれば、実システムでも（その後）真です。逆に、刻々と変わる瞬間的な値（ある一瞬の総スループットなど）の厳密測定には向きません。

ローカルなWAL/チェックポイントとの違い

単一ノードのWAL（先行書き込みログ）やチェックポイント機構は、1台の中の一貫性を扱います。Chandy-Lamport が解くのはそれらを横断した、ノード間にまたがる一貫性です。各ノードが勝手にローカルチェックポイントを取ると、復旧時に「受信は残るが送信は消えた」孤児メッセージや、復旧連鎖が際限なく巻き戻るドミノ効果が起こり得ます。協調的（coordinated）チェックポイントとして Chandy-Lamport 型のマーカーを使えば、全体が一斉に一貫した断面で固定され、これらを構造的に防げます。

時刻でなく因果順序で一貫性を組み立てる発想は、論理クロックの系譜と地続きです。マーカーの代わりにベクタークロックやハイブリッド論理クロック(HLC)とTrueTimeで「読みたい時点」を境界として与える手法もあり、いずれも「全ノード共通の今」が無い世界で一貫した断面をどう定義するか、という同じ問いに答えています。スナップショットを保存して障害から全体を再開する考え方は、分散合意（Paxos / Raft）でログを揃える発想とも補完的に働きます。

まとめ