要約

  • happened-beforeは、各プロセス内の順序、同じメッセージの送信から受信への辺、そして推移閉包から作られる最小の半順序である。
  • Clock Conditionは一方向だけを保証する。a → bならC(a) < C(b)でなければならないが、小さいスカラー値だけでaがbを引き起こした、知らせた、物理的に先だったとは証明できない。
  • 双方向にhappened-before経路がない事象は並行である。それは観測モデル内で順序がないという意味で、壁時計上の同時刻ではない。後のベクトル時計はこの比較不能性をより忠実に残す。

二つのサービスが決定的に見える記録を残す。事象Aの論理時刻は41、Bは42だ。画面は行を並べ、矢印を引き、AがBを引き起こしたように見せる。数字は説明を簡単にするが、証拠を増やしてはいない。

Leslie Lamportが1978年に発表した Time, Clocks, and the Ordering of Events in a Distributed System は、隠れた万能時計を見つける論文ではなかった。大域時計がない環境で、システムが正当に主張できる順序を限定した仕事だった。

観測可能な辺から作る最小の半順序

Lamportは、事象列を持つ複数のプロセスがメッセージで結ばれるモデルを置く。happened-beforeは三つの規則を満たす最小の関係だ。同じプロセスでは早い事象が遅い事象に先行する。メッセージの送信は同じメッセージの受信に先行する。aがbに、bがcに先行すれば、aはcに先行する。

「最小」であることが重要だ。規則が要求しない空白は推測で埋めない。a → bでもb → aでもない二つの事象は並行であり、モデルは見栄えのよい一本の時間線のために先後を発明しない。

Lamportはa → bを、aがbへ因果的に影響し得ることだと説明する。局所ステップとメッセージ辺を通じて情報が届き得る、という到達可能性である。aの業務内容が実際にbの結果を変えたこと、誰かがそれを意図したこと、責任が確定したことまでは含まない。経路の存在と意味上の原因は別の証拠だ。

何を一つの事象とするかも順序を変える。論文の脚注は、受信を割り込みビットの設定とみなすか、割り込み処理の実行とみなすかで受信事象の順序が変わると指摘する。順序を問う前に、事象定義の版を問う必要がある。

Clock Conditionは同値関係ではない

論理時計は各事象に数を割り当てる。Clock Conditionは、a → bならC(a) < C(b)であるべきだと定める。各プロセスは連続する事象の間でカウンターを進め、送信時の値をメッセージに載せ、受信時には自分の現在値と受信値の両方より後へ進める。

この規則は既知の矢印が数値上で逆向きになるのを防ぐ。しかし逆は言えない。C(a) < C(b)だけからa → bは導けない。

これは実装の粗さではなく、スカラー表現の境界である。数値比較のすべてをhappened-beforeと同一視すると、並行な事象は同じ値を持たなければならない。ところが一つの事象が、別プロセス内で互いに順序づけられた二つの事象の両方と並行になる場合があり、三者を同値にすると局所順序に反する。

スカラー時計が証明するのは、既知の因果辺が保たれたことだ。値が増えたすべての組に因果辺があることではない。

全順序は世界の復元ではなく決定規則

半順序が複数の答えを許す場面でも、システムは一つを選ばなければならないことがある。Lamportは論理時刻で並べ、同値なら固定したプロセス順で決める方法を示した。得られる全順序はhappened-beforeと矛盾しない。

だが一意ではない。別の適格な時計や別の同順位規則は別の線形順序を作れる。事象系から一意に定まるのは半順序だけである。

キューや複製サービスが決定的な順序を採用すること自体は正しい。必要なのは、その部分を制御方針として記録することだ。同順位規則を過去の発見として扱えば、運用上の選択が偽の歴史事実になる。

ログの外にあった電話

論文の「異常な振る舞い」の例は、観測境界を端的に示す。ある人がコンピューターAで要求Aを出し、別の都市の友人に電話し、Bで要求Bを出してもらう。電話は計算機システムの外にあるため、Bが小さいタイムスタンプを得てAより前に並ぶことがある。

内部事象しか見ないアルゴリズムは、観測しなかった辺を復元できない。Lamportは、欠けた順序情報を明示的にシステムへ持ち込むか、より強い仮定の下で十分に同期した物理時計を使う道を示す。

現代なら、欠けた辺はサポート電話、人の承認、webhook、外部キューかもしれない。「経路なし」は「この記録集合に経路がない」という結論であり、現実に影響がなかった証明ではない。

論理時刻、ベクトル時刻、物理時刻

Lamportのスカラー時計はClock Conditionの前向き含意を保ち、整合した全順序を作れる。約十年後、Colin FidgeとFriedemann Matternは、半順序をより多く残すベクトル時刻を発展させた。Matternは、半順序の事象を線形な整数へ写すと、並行であり得る事象に異なる値を与え、情報を失うと論じた。

どちらも相手の因果過去にない場合、ベクトルは比較不能のままにできる。デバッグ、スナップショット、競合判断には重要だ。それでも記録済みのプロセス、事象、メッセージ辺に依存し、記録外の電話や人の動機は発見しない。

物理時計は別の問いに答える。Lamport自身の論文も、Strong Clock Condition、時計速度の誤差、ドリフト、メッセージ最小遅延、同期限界を扱う。これらの仮定は時刻ラベルを物理時間へ近づけるが、論理カウンターを壁時計にはせず、固有の不確かさを伴う。

著者の境界も同じ精度で守るべきだ。Lamportは1978年にhappened-beforeとスカラー論理時計を定式化し、Paul JohnsonとBob Thomasによる先行するメッセージ時刻の着想を明記した。ベクトル時計はFidgeとMatternの後続研究である。

順序の主張に必要な記録

検証可能な調査は、事象定義と版、プロセス、局所番号、メッセージID、送受信の対応、時計アルゴリズム、観測範囲を示す。物理的先後を主張するなら時計源と誤差を、原因を主張するなら結果を変えた仕組みの証拠を追加する。

結論は複数に分けられる。取得モデル内のhappened-before、同モデル内の並行、同順位規則で先に置かれた、指定誤差内で物理的に早い、意味上の原因は未証明、である。

Lamportの貢献は、すべてを並べて真実と呼ぶ許可ではない。システムが知る順序、選ぶ順序、まだ証明できない順序を分離する方法である。

情報源