Mercurial > hg > Papers > 2009 > rep-verify-sigos

comparison rep-verify-sigos.ind @ 4:8e30bfb5deb6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Mar 2009 12:53:57 +0900
parents f1214f4b5933
children
comparison
equal deleted inserted replaced
3:f1214f4b5933 4:8e30bfb5deb6
9 を実現するとともに、複雑なプロトコルをSession Manager側に閉じ込めて、 9 を実現するとともに、複雑なプロトコルをSession Manager側に閉じ込めて、
10 Editor側の実装の手間を軽くすることを提案する。 10 Editor側の実装の手間を軽くすることを提案する。
11 11
12 一方で、プロトコル自体がかなり複雑になったので、プロトコルの正しさ 12 一方で、プロトコル自体がかなり複雑になったので、プロトコルの正しさ
13 及び、プロトコル実装の正しさを検証する必要が出て来た。 13 及び、プロトコル実装の正しさを検証する必要が出て来た。
14 プロトコル検証では、Java PathFinder\cite{javapathfinder}の 14 プロトコル検証では、Java PathFinder\cite{havelund98model}の
15 有効性が知られているが、それを用いるために、ソケット 15 有効性が知られているが、それを用いるために、ソケット
16 通信をThread間の同期で実現するライブラリを作成した。 16 通信をThread間の同期で実現するライブラリを作成した。
17 また、Editor側の実装の正しさの検証及びデバッグのために、 17 また、Editor側の実装の正しさの検証及びデバッグのために、
18 テスト用のEditorを作成した。 18 テスト用のEditorを作成した。
19 19
39 複雑なコマンド入力などのない\underline{Simple なユーザInterface}。 39 複雑なコマンド入力などのない\underline{Simple なユーザInterface}。
40 これらを実現するために\underline{Conflictを非同期に解決}し、 40 これらを実現するために\underline{Conflictを非同期に解決}し、
41 変更の伝播の遅延は容認する。また、 41 変更の伝播の遅延は容認する。また、
42 \underline{小人数向け}の共有とする。遅延を容認するために、 42 \underline{小人数向け}の共有とする。遅延を容認するために、
43 \underline{遠距離でも使用可能}となる。また、オープンソースとして実装し、 43 \underline{遠距離でも使用可能}となる。また、オープンソースとして実装し、
44 \underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{xp} 44 \underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{bib:xp}
45 における\underline{Pair Programming}での使用を意識しているので、 45 における\underline{Pair Programming}での使用を意識しているので、
46 \underline{Emacs/vim/Eclipseの相互接続}を重視する。 46 \underline{Emacs/vim/Eclipseの相互接続}を重視する。
47 将来的には、動的な変更を可能とする 47 将来的には、動的な変更を可能とする
48 \underline{Inter-Application Protocol}として使えるものを 48 \underline{Inter-Application Protocol}として使えるものを
49 目指している。 49 目指している。
139 次のMerge Protocolでは、SM上でEditorのコマンドのundoを計算する 139 次のMerge Protocolでは、SM上でEditorのコマンドのundoを計算する
140 必要があるので、{\tt user\_delete}には、削除した行の内容が 140 必要があるので、{\tt user\_delete}には、削除した行の内容が
141 付加されてSMに送られる。したがって、{\tt user\_delete}と 141 付加されてSMに送られる。したがって、{\tt user\_delete}と
142 {\tt user\_insert}と見掛け上対称となる。 142 {\tt user\_insert}と見掛け上対称となる。
143 143
144 全文置換なども{\tt user\_inert, user_delete}に分解する必要が 144 全文置換なども{\tt user\_inert, user\_delete}に分解する必要が
145 あり、その分解はEditorによって行なわれる。REPは歴史的理由で行指向の 145 あり、その分解はEditorによって行なわれる。REPは歴史的理由で行指向の
146 プロトコルであり、行指向でないEditorでも行番号を付加する 146 プロトコルであり、行指向でないEditorでも行番号を付加する
147 必要がある。 147 必要がある。
148 148
149 {\tt sync}に対しては、要求された行に対して、 149 {\tt sync}に対しては、要求された行に対して、
162 162
163 REPでは、二つのEditorの場合の編集の衝突の解決を行なう 163 REPでは、二つのEditorの場合の編集の衝突の解決を行なう
164 手法を提案して来た。この方法(Merge Protocol (A))では自分のEditor Commandを 164 手法を提案して来た。この方法(Merge Protocol (A))では自分のEditor Commandを
165 相手に送り、戻って来るまでのEditor Commandをキューに入れておく。 165 相手に送り、戻って来るまでのEditor Commandをキューに入れておく。
166 他のEditorのCommandを受け取った時には、その 166 他のEditorのCommandを受け取った時には、その
167 キューと、そのCommandの可換性を調べて、キューを変更する\cite{}。 167 キューと、そのCommandの可換性を調べて、キューを変更する\cite{kono04g}。
168 しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。 168 しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。
169 169
170 そこで、以下のようなMerge Protocol (B)を導入する。(1) Editor Command 170 そこで、以下のようなMerge Protocol (B)を導入する。(1) Editor Command
171 をSession Ring 上に流し、それが戻って来るまでに、他のEditorから 171 をSession Ring 上に流し、それが戻って来るまでに、他のEditorから
172 受け取った Editor Command をキューに入れておく。 172 受け取った Editor Command をキューに入れておく。
216 これを防ぐ一つの方法は、Merge 作業が始まった段階で、ユーザ入力を 216 これを防ぐ一つの方法は、Merge 作業が始まった段階で、ユーザ入力を
217 block してやれば良い(a)。もう一つの方法は、ユーザ入力の割り込みが 217 block してやれば良い(a)。もう一つの方法は、ユーザ入力の割り込みが
218 あった場合は、その入力込みで、もう一度、ソートを実行すれば良い(b)。 218 あった場合は、その入力込みで、もう一度、ソートを実行すれば良い(b)。
219 これはリマージと呼ばれる。 219 これはリマージと呼ばれる。
220 220
221 <center><img src="fig/remerge.pdf" alt="リマージ"></center> 221 <center><img src="fig/reMerge.pdf" alt="リマージ"></center>
222 222
223 Merge 作業中には、他のSM/Editorからの入力をblockすることは問題ない。 223 Merge 作業中には、他のSM/Editorからの入力をblockすることは問題ない。
224 それは、もともと非同期で動作しており、遅延は許容されるように 224 それは、もともと非同期で動作しており、遅延は許容されるように
225 なっている。 225 なっている。
226 226
249 % $C_{ij}$の$j$は、{\tt NOP}を含めた番号に付け換える。 249 % $C_{ij}$の$j$は、{\tt NOP}を含めた番号に付け換える。
250 250
251 Editor $m$では、 251 Editor $m$では、
252 \[ C_{m0} C_{x0} N_{00} .... N_{yz} \] 252 \[ C_{m0} C_{x0} N_{00} .... N_{yz} \]
253 などのコマンド列が実行されることになる。これを$C/N$の 253 などのコマンド列が実行されることになる。これを$C/N$の
254 区別のないコマンド記号(E_{ij})で置き換えよう。 254 区別のないコマンド記号($E_{ij}$)で置き換えよう。
255 \[ E_{m0} E_{x0} E_{00} .... E_{yz} \] 255 \[ E_{m0} E_{x0} E_{00} .... E_{yz} \]
256 NOPの付加手順から、 256 NOPの付加手順から、
257 他のEditorが送ったCommandには、その前の他のEditorからのCommandを 257 他のEditorが送ったCommandには、その前の他のEditorからのCommandを
258 受け取った後の、 258 受け取った後の、
259 自分が送ったCommand(0以上の複数個) 259 自分が送ったCommand(0以上の複数個)
297 の前に挿入されていると考えて良い。従って、(A)と同じように集合列$Z$ 297 の前に挿入されていると考えて良い。従って、(A)と同じように集合列$Z$
298 を、すべてのEditorで同一となるように決めることが出来る。 298 を、すべてのEditorで同一となるように決めることが出来る。
299 299
300 プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、 300 プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、
301 このように簡単に証明することは出来ない。そこで、 301 このように簡単に証明することは出来ない。そこで、
302 モデル検査器であるJava PathFinder\cite{}を用いる。 302 モデル検査器であるJava PathFinder\cite{havelund98model}を用いる。
303 303
304 --Protocol の実装 304 --Protocol の実装
305 305
306 Session Manager はJava 1.5で実装されており、 Ecplise は Java によるPlug-in 306 Session Manager はJava 1.5で実装されており、 Ecplise は Java によるPlug-in
307 となっている。 Emacs は、従来はCで書いたクライアントを接続していたが、 307 となっている。 Emacs は、従来はCで書いたクライアントを接続していたが、
311 今回の実装では、Editor 側の実装のコストが削減されており、Merge Protocol 311 今回の実装では、Editor 側の実装のコストが削減されており、Merge Protocol
312 部分でCで150行程度が削減されている。Editor 側の実装は、Editor Command を 312 部分でCで150行程度が削減されている。Editor 側の実装は、Editor Command を
313 {\tt insert, delete} に分解する部分の実装が大半である。 313 {\tt insert, delete} に分解する部分の実装が大半である。
314 314
315 Editor 側で実装する必要があるのは、表\ref{tb:sync}の機能である。 315 Editor 側で実装する必要があるのは、表\ref{tb:sync}の機能である。
316 \end{table}
317 \begin{table}[htdp] 316 \begin{table}[htdp]
318 \caption{Editor 側での実装} 317 \caption{Editor 側での実装}
319 \begin{center} 318 \begin{center}
320 \begin{tabular}{|l|l|} 319 \begin{tabular}{|l|l|}
321 \hline 320 \hline
327 \hline 326 \hline
328 4 & {\tt join\_ack,put\_ack} の受け取りとsid,eidの設定 \\ 327 4 & {\tt join\_ack,put\_ack} の受け取りとsid,eidの設定 \\
329 \hline 328 \hline
330 5 & 外部からのEditor Commandの非同期受け取りと実行 \\ 329 5 & 外部からのEditor Commandの非同期受け取りと実行 \\
331 \hline 330 \hline
332 6 & {\tt sync} Command を受け取った場合の{\tt user\_insert,user\_detele}の生成 331 6 & {\tt sync} Command を受け取った場合の{\tt user\_insert,user\_detele}の生成 \\
333 \hline 332 \hline
334 7 & Merge 時のlock (optional) \\ 333 7 & Merge 時のlock (optional) \\
335 \hline 334 \hline
336 7 & {\tt quit} Command \\ 335 7 & {\tt quit} Command \\
337 \hline 336 \hline
395 Sample Editor に対する動作を確認することで調べることが出来る。 394 Sample Editor に対する動作を確認することで調べることが出来る。
396 395
397 396
398 --比較 397 --比較
399 398
400 類似のProject としては、GroupKit \cite{}, Soba Project\cite{} がある。 399 類似のProject としては、GroupKit \cite{bib:groupkit}, Soba Project\cite{bib:soba} がある。
401 vim やEmacs などのOpen source editor の実装を含むのが、REPの特徴 400 vim やEmacs などのOpen source editor の実装を含むのが、REPの特徴
402 である。 401 である。
403 402
404 また、Java で実装されていて、Session Manager 部分、Editor の改変部分、 403 また、Java で実装されていて、Session Manager 部分、Editor の改変部分、
405 Eclipse plugin のすべてが、LGPLで公開されているのも独自な特徴の 404 Eclipse plugin のすべてが、LGPLで公開されているのも独自な特徴の
409 Java の部分をJava PathFinder で検証することが可能だと思われる。 408 Java の部分をJava PathFinder で検証することが可能だと思われる。
410 しかし、現状では、まだ、検証までには至っていない。 409 しかし、現状では、まだ、検証までには至っていない。
411 410
412 GroupKit などで使われているマルチメディア編集の同期は、Masterが 411 GroupKit などで使われているマルチメディア編集の同期は、Masterが
413 一つ存在し、それに対するCommandの発行と、MasterからのCommandの 412 一つ存在し、それに対するCommandの発行と、MasterからのCommandの
414 マルチキャストで実現されている\cite{}。REPでは、マルチキャスト 413 マルチキャストで実現されている\cite{bib:ellis}。REPでは、マルチキャスト
415 ではなく、Session ring によって同期を実現している。Ring は、 414 ではなく、Session ring によって同期を実現している。Ring は、
416 遅く信頼性に欠ける部分があるが、ネットワークに対する負荷が 415 遅く信頼性に欠ける部分があるが、ネットワークに対する負荷が
417 軽いと言う特徴がある。(C)のMerge Protocolを使うことにより、 416 軽いと言う特徴がある。(C)のMerge Protocolを使うことにより、
418 o(n)のパケットで同期を行なうことが出来る。また、マルチキャスト 417 o(n)のパケットで同期を行なうことが出来る。また、マルチキャスト
419 を避けているので、WANなどの遅延が大きい部分に複数のストリーム 418 を避けているので、WANなどの遅延が大きい部分に複数のストリーム
423 大きなファイルを編集する場合でも、Session Manager のメモリを 422 大きなファイルを編集する場合でも、Session Manager のメモリを
424 消費することはない。 423 消費することはない。
425 424
426 --最後に 425 --最後に
427 426
428 このプロジェクトは、sourceforge を通じて公開\cite{}されており、まだ、 427 このプロジェクトは、sourceforge を通じて公開\cite{rep-sourceforge}されており、まだ、
429 開発途上となっている。 428 開発途上となっている。
430 429
431 残念ながら、実際のSession Manager 上でのJava Pathfinder での検証は 430 残念ながら、実際のSession Manager 上でのJava Pathfinder での検証は
432 まだ、出来てはないが、通信ライブラリ上での処理をatomicにするなどの 431 まだ、出来てはないが、通信ライブラリ上での処理をatomicにするなどの
433 工夫で可能になると期待している。 432 工夫で可能になると期待している。