本プログラムは、以下のような構成を取っている。
- 端のデータを交換
- 更新可能な部分のデータを更新
- 更新したインデックスと残差を一台のプロセッサで集計
ここでプログラムの実行はループごとに分離できるため、一回分のループが
正しく全てのインデックス範囲について実行されることを示す。
一回のループが回るということは、全ての断片のデータが更新可能になる、と読み替えることができる。
この条件は、初期状態から始まり、最終的に任意の要素に隣接するデータが、その要素が属する断片内に存在すればよい。
まず、記法の定義を行う。
(集合) ← (メソッドの種類, 引数)
:メソッドを(集合)に対し呼び出す
S : インデックス集合
D : インデックス集合と、それに対応するデータ (map)
D.S : Dに付随するインデックス集合
D[S0]: Dのうち、S0のインデックス範囲に相当するものを返す
adjacent(S) : Sの端に隣接するインデックス集合
edge(S) : Sの端のインデックス集合
ここで、adjacent, edgeについては以下の性質を持つものとする。
∀Sa⊂S, adjcent(Sa)⊂ adjcent(S) ∪ S
これを元に、以下のコードを検証する。
class F{
S : インデックス集合
D : データ集合
m_s(){
adjacent(S) ← (m_r, D[edge(S)])
}
m_r(D_r){
D += D_r
}
split(){
S → S0, S1
D0 = D[S0 ∪ (adjacent(S0) ∩ D.S)]
D1 = D[S1 ∪ (adjacent(S1) ∩ D.S)]
S = S0; D = D0
return S1, D1
}
merge(S0, D0){
S += S0
D += D0
}
};
main(){
各断片がSk, Dkを持ち、ΣSk == S_whole, Sk == Dk.S
S_whole ← (m_s)
}
ここで、split(), merge()がメソッド実行の途中の任意のタイミングで呼ばれる。
また、一度呼ばれたRMI要求は必ず実行され、split()が行われると必ず対応するmerge()がいずれ呼ばれるものとする。
示すこと
最終的に
∀e∈S, adjacent(e) ⊂ D.S
Sの要素eについて、その上下左右の隣接要素は全てDに含まれる
上記の証明すべき命題は、以下のように書き換えられる
(A) 途中のあらゆる遷移状態において、
∀e0, e1 | e1 ∈adjacent(e0)
( S_whole中の隣接する要素の組e0, e1 )
について、以下の三つのいずれかが成立する。
(1): e1 ← (m_s)というRMIメッセージが存在
(2): e0 ← (m_r, e1のデータ)というRMIメッセージが存在
(3): e0 ∈ S, e1 ∈ D.S (となる断片が存在)
(B)上の1や2の状態は3に移行する
split()---merge()の遷移状態では、転送中の「断片」についてこれらの性質が成り立てばよいてする。
まず(A)を示す。
-
初期状態においては、S_wholeに対してm_sが呼び出されているので、
∀e0について(1)が成立する。
-
m_sの呼び出しを受けた断片では、
adjacent(S) ← (m_r, D[edge(S)])
という操作を行う。注目しているメッセージではe1∈Sである。
ここでadjacentについての性質から、
e0 ∈ adjcent(e1)よりe0 ∈ S ∪ adjacent(S)
が成立する。
ここで、e0∈adacent(S)であれば、e1←(m_r, e1のデータ)というメッセージ送信されることになり、
(e0, e1)の組に対し(2)が成立する。
また、e0がadacent(S)に含まれないときは、e0∈Sとなるので、(3)が成立する。
-
m_rの呼び出しを受けた断片では、
D += (引数のデータ)
という操作を行う。ここで、(2)のメッセージは引数にe1のデータを含むので、この操作によりe1∈D.Sが成立するようになる。つまり、(3)が成立する
-
split(), merge()は任意のタイミングで呼び出される。ここで、これらの操作によって(1)や(2)の状態は変化しない。(3)が成立していたとき、これがsplit()によってもmerge()によっても変化しないことを示す。
(3): e0 ∈ S, e1 ∈ D.S (となる断片が存在)
---
split(){
S → S0, S1
D0 = D[S0 ∪ (adjacent(S0) ∩ D.S)]
D1 = D[S1 ∪ (adjacent(S1) ∩ D)]
S = S0; D = D0
return S1, D1
}
merge(S0, D0){
S += S0
D += D0
}
まずsplit()だが、e0 ∈S0として一般性を失わない。
e1 ∈ adjacent(e0)より、e1 ∈ S0 ∪ (adjacent(S0) ∩ D.S)となるので、e1 ∈ D0.Sとなる。
つまり、split()によって(3)の性質は失われない。
また、merge()においては、(e_a ∈ Saであればe_a ∈ Sa + Sb)より(3)は失われない。
これにより、(A)が示された。
次に(B)だが、起こりうる状態遷移は
で、(1)や(2)はメッセージを伴う状態でいずれかは次の状態に遷移するので、最終的に(3)に収束するとしてよい。
これらにより、証明すべき命題が示された。