分散処理のモデル化

『Distributed Algorithms for Message-Passing Systems』第六章「Nature of Distributed Computations and the Concept of a Global State」にて定義されている分散処理モデル化手法の要約。
ここに記述されている内容が後続の章に何度か登場するのでまとめておきます。

分散処理をモデル化するための３つの方法

逐次実行は連続するローカル状態の列や、初期状態 + ステートメントの列を用いてモデル化できる。
分散処理であれば、以下を用いてモデル化することが可能である。

ローカルイベントの集合とそれらの半順序関係
ローカル状態の集合とそれらの半順序関係
グローバル状態の格子

ローカルイベントの集合とそれらの半順序関係を利用したモデル

イベント

プロセスによるステートメントの実行。分散システムにおけるイベントは、以下の三種に分類される。

メッセージの送信イベント
メッセージの受信イベント
内部イベント
- 他プロセスとの通信を行わないイベント

プロセス履歴

特定の一つのプロセスによる実行履歴を以下のように定義する。

e_i^x = p_i が生成する x 番目のイベント \\
h_i = p_i が生成するイベントの集合 \\
\to_i = h_i に含まれるイベントの全順序 \\
\hat{h_i} = (h_i, \to_i) = e_i^1, e_i^2, …, e_i^x, e_i^{x+1}, … = p_i の履歴

メッセージ送受信関係

分散処理中に送受信されたメッセージの集合を $M$、メッセージの送受信関係を $\to_{msg}$ とする。
$m \in M$ であるとき、$s(m)$ をそのメッセージの送信イベント、$r(m)$ を受信イベントとすると、$s(m) \to_{msg} r(m)$ が成り立つ。

イベント同士の順序関係

$\xrightarrow{ev}$ をイベントの順序とする。これは因果先行関係(本ではこちらが使用されている)や happened before関係(こちらの方が意味的には正確)と呼ばれる。
$e_i^x \xrightarrow{ev} e_j^y$ は以下のいずれかを満たす。

$i = j \land x < y$
- $e_i^x$、$e_j^y$ は同一プロセスが生成したイベントで、前者が後者に先行している
$\exists m \in M: e_i^x = s(m) \land e_j^y = r(m)$
- メッセージの送受信関係
$\exists e: e_i^x \xrightarrow{ev} e \land e \xrightarrow{ev} e_j^y$
- 推移関係

また、因果関係のないイベントは並行であり、以下のように表現する。

$a || b = \lnot(a \xrightarrow{ev} b) \land \lnot(b \xrightarrow{ev} a)$

分散処理モデル

分散処理中に生成されたすべてのイベントの集合を、$H_i$ とする。

$H_i = \cup_{1<=i<=n}h_i$

これとイベント間の順序関係を用いて、分散処理を以下のようにモデル化する。
２つの分散実行が同じイベントの集合と半順序関係から成り立っている場合、仮にイベントが生成された物理時刻が違えど、同じ分散実行であるとみなすことができる。

$\hat{H_i} = (H_i, \xrightarrow{ev})$

ローカル状態とそれらの半順序関係を利用したモデル

ローカル状態

プロセス $p_i$ の初期状態を $\sigma_i^0$ とする。これに最初のイベント $e_i^1$ を適用すると、ローカル状態は $\sigma_i^1$ に推移する。
さらに一般化し、イベント $e_i^x$ はローカル状態 $\sigma_i^{x-1}$ を $\sigma_i^x$ に推移させると考える。このようにすると、イベント列からローカル状態が計算できる。
この本では、ローカル状態の推移を以下のように表記することがある。

$\sigma_i^x = \delta(\sigma_i^{x-1}, e_i^x)$

イベント順序の拡張

$\xrightarrow{ev}$ を拡張した $\xrightarrow{ev'}$ を定義する。
これは、 $\xrightarrow{ev}$ を満たすための条件 $i = j \land x < y$ を $i = j \land x <= y$ に緩めたものである。
これにより、あるイベントはそのイベント自体に先行しているとみなすことができる。

ローカル状態の順序関係

$S$ を分散実行により生じるすべてのローカル状態とする。
また、ローカル状態同士の順序 $\xrightarrow{\sigma}$ を定義する。

$\sigma_i^x \xrightarrow{\sigma} \sigma_j^y = e_i^{x+1} \xrightarrow{ev'} e_j^y$

$e_i^{x+1}$ がメッセージの送信イベントで $e_j^y$ が受信イベントである場合
- $e_i^{x+1}$ に先行している $\sigma_i^x$ は、$e_j^y$ によって生成される $\sigma_j^y$ に先行する
$e_i^{x+1}$ と $e_j^y$ が同一プロセスで発生し、かつ $y = x + 1$ である場合
- $e_i^{x+1} = e_j^y$ に先行している $\sigma_i^x$ は、$e_j^y$ が生成する $\sigma_j^y = \sigma_i^{x+1}$ に先行している

また、並行なローカル状態同士を以下のように表現する。

$\sigma1 || \sigma2 = \lnot(\sigma1 \xrightarrow{\sigma} \sigma2) \land \lnot(\sigma2 \xrightarrow{\sigma} \sigma1)$

分散処理モデル

分散処理はローカル状態とそれらの半順序を用いて以下のようにモデル化できる。

$\hat{S} = (S, \xrightarrow{\sigma})$

グローバル状態の格子を利用したモデル

グローバル状態と整合グローバル状態

グローバル状態(スナップショット)は $n$ 個のローカル状態で表現できる。

$\sum = [\sigma_i, …, \sigma_i, …, \sigma_n]$

また、各ローカル状態が以下を満たすグローバル状態を、整合グローバル状態とする。

$\forall i,j : i \neq j => \sigma_i || \sigma_j$

言い換えると、整合グローバル状態はそれぞれのローカル状態が因果的に依存していないグローバル状態である。

グローバル状態の到達可能性

整合グローバル状態 $\sum_1 = [\sigma_1, …, \sigma_i, …, \sigma_n]$ に $e_i$ を適用したグローバル状態 $\sum_2 = [\sigma_1', …, \sigma_i', …, \sigma_n']$ が以下を満たすとき、 $\sum_2$ は $\sum_1$ から直接到達可能である。

$\forall j \neq i: \sigma_j' = \sigma_j$
$\sigma_i' = \delta(\sigma_i, e_i)$

したがって、整合グローバル状態 $\sum_2 = [\sigma_1, …, \delta(\sigma_i, e_i), …, \sigma_n]$ は整合グローバル状態 $\sum_1 = [\sigma_1, …, \sigma_i, …, \sigma_n]$ から直接到達可能である。これを $\sum_2 = \delta(\sum_1, e_i)$ と表現する。

また $\sum_1$ から $\sum_z$ に推移的に到達できる場合、$\sum_z$ は $\sum_1$ から到達可能である。これを $\sum_1 \xrightarrow{\sum} \sum_z$ と表記する。

分散処理モデル

直接到達可能な整合グローバル状態同士をイベントで結んだグラフを到達可能性グラフとする。
到達可能性グラフは格子状の構造を持つ。つまり、任意の２つの頂点は単一の最大共通祖先、単一の最小共通子孫を持つ。
分散処理はこの到達可能性グラフを用いてモデル化することができる。
到達可能性グラフは、分散実行が通りうるすべての整合グローバル状態を含んでいる。