Mercurial > hg > Papers > 2009 > rep-verify-sigos
comparison 4.tex @ 5:34bfeb51e287
add section tex file, Makefile
| author | gongo@gendarme.local |
|---|---|
| date | Sat, 28 Mar 2009 16:26:43 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 4:8e30bfb5deb6 | 5:34bfeb51e287 |
|---|---|
| 1 \section{ Protocol の正しさ} | |
| 2 | |
| 3 Merge Protocol の正しさの証明は、Protocol自体の正しさと、 | |
| 4 Protocolの実装を含めた正しさの二種類の正しさを示す必要がある。 | |
| 5 | |
| 6 ここでは、(A)のProtocolの正しさを示す。Editor $0..n$ が、 | |
| 7 それぞれ、編集コマンド$C_{ij}$ (Editor $i$の$j$番目のコマンド,$j$は0から)を | |
| 8 入力したとする。このコマンドは、Session ring を巡回する。 | |
| 9 巡回するたびに、各Editor $k$が{\tt NOP} Command $N_{kx}$を、その | |
| 10 コマンドの前に付加する。 | |
| 11 % (A)では自分が既にCommandを送っていれば{\tt NOP}を付加する必要は | |
| 12 % ないが、ここでは、必ず付加することにする。 | |
| 13 $x$は、コマンドの順序である。 | |
| 14 % $C_{ij}$の$j$は、{\tt NOP}を含めた番号に付け換える。 | |
| 15 | |
| 16 Editor $m$では、 | |
| 17 \[ C_{m0} C_{x0} N_{00} .... N_{yz} \] | |
| 18 などのコマンド列が実行されることになる。これを$C/N$の | |
| 19 区別のないコマンド記号($E_{ij}$)で置き換えよう。 | |
| 20 \[ E_{m0} E_{x0} E_{00} .... E_{yz} \] | |
| 21 NOPの付加手順から、 | |
| 22 他のEditorが送ったCommandには、その前の他のEditorからのCommandを | |
| 23 受け取った後の、 | |
| 24 自分が送ったCommand(0以上の複数個) | |
| 25 または、{\tt NOP} | |
| 26 が必ず対応している。 | |
| 27 対応するCommandとは、Session ring 上で同時に実行されたと考えられる | |
| 28 Command の集合と考えて良い。 | |
| 29 Command はSession ring を一周するので、すべての | |
| 30 Editor が同じCommandの集合を受け取っている。 | |
| 31 | |
| 32 ここで、対応したCommandの集まり毎に列を分割し、 | |
| 33 Editor iの | |
| 34 その集まりを集合と | |
| 35 みなし$S_{ij}$ とする。この集合の列を$Z_i$とする。 | |
| 36 \[ Z_i = S_{i0} S_{i1} .... S_{in} \] | |
| 37 定義から隣同士の$S_{ij}$には、 | |
| 38 対応したCommandが含まれることはない。 | |
| 39 | |
| 40 この集合列$Z$は、すべてのEditorで同一となる。 | |
| 41 [証明] | |
| 42 Editor $i$とEditor $j$で、$S_{ik}$と、$j$の$S_{jk}$が異なっている | |
| 43 としよう。あるCommand $E_s$があって、 | |
| 44 $E_s \in S_{ik}$であって$E_s \in S_{jk}$でない。 | |
| 45 しかし、$E_s$ | |
| 46 はsession ringを一周しているので、$S_{ik}$と$S_{jk}$の両方に | |
| 47 含まれているか、隣同士にあるはずである。両方に含まれていると | |
| 48 すると仮定と矛盾するので、隣同士になるはずである。しかし、隣同士で | |
| 49 あれば、Command の分割の方法に矛盾する。[証明終り] | |
| 50 | |
| 51 従って、$S_i$をEditor idとCommand順序によってソートしてやれば、 | |
| 52 すべてのEditorで、同一なCommand列を得ることが出来る。 | |
| 53 ソートのタイミングは、対応するコマンドがすべて自分に到着した時点である。 | |
| 54 自分の送った新しいコマンド、または、新しい{\tt NOP}が | |
| 55 来たことによって、その一つ前までが対応しているものだということがわかる | |
| 56 ので、その時点でソートしてやれば良い。従って、Merge Protocolにより、 | |
| 57 すべてのEditorで同一の編集結果が得られることがわかった。 | |
| 58 | |
| 59 (B)では、{\tt NOP}の挿入の代わりに{\tt ack}を、もう一周させている。 | |
| 60 {\tt ack} が来た時点で、対応するCommandの集合が確定する。あるいは、 | |
| 61 仮想的に{\tt NOP}を挿入したと考えると、その{\tt NOP}は、{\tt ack} | |
| 62 の前に挿入されていると考えて良い。従って、(A)と同じように集合列$Z$ | |
| 63 を、すべてのEditorで同一となるように決めることが出来る。 | |
| 64 | |
| 65 プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、 | |
| 66 このように簡単に証明することは出来ない。そこで、 | |
| 67 モデル検査器であるJava PathFinder\cite{havelund98model}を用いる。 | |
| 68 |