Papers/2009/rep-verify-sigos: rep-verify-sigos.ind comparison

comparison rep-verify-sigos.ind @ 3:f1214f4b5933

figure

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 26 Mar 2009 10:31:47 +0900
parents	ac15ac2df491
children	8e30bfb5deb6

comparison

equal deleted inserted replaced

-:ac15ac2df491
+:f1214f4b5933
 複数人が同じテキストを共有して編集するプロトコルは、
 さまざまなものが提案されているが、汎用エディタに実装
 する前堤のプロトコルはほとんどない。Remote Editing Protocol
 では、複数のSession Managerと、リング状のSession の上に
 編集コマンドを循環させる方法を取っている。
+<center><img src="fig/editor_to_editor2.pdf" alt="REPでの相互接続"></center>
 この方法を採用した理由はいくつがある。
 集中サーバを用いない\underline{分散実装}が一つの前堤になっている。
 Session Manager 自体が分散していて、Session Manager は、
 (分離されたMergerを除けば)編集コマンドを中継するだけである。
 は自動的に決まったポートを通してSMに接続(join/put)する。このようにすれば、
 エディタ上でホスト名を入力する必要はない。一つのホスト上では、
 単一のSMに複数のエディタが接続する。離れたホスト同士のエディタを
 接続する場合は、まず、それぞれのホスト同士のSMを接続する。そして、
 それぞれエディタがSMに接続した後で、ホスト間の接続を選択(select)する。
+<center><img src="fig/one_session_manager.pdf" alt="Session Managerの導入"></center>
 ---Session managerの接続protocol
 SM同士の接続は、{\tt sm\_join}コマンドをSMに送ることによる。
 接続により、接続したSM間でuniqueな session manager id
 が発行される場合もあるので、リングを避けるために、
 {\tt sm\_join} はmaster SMまで転送される。自分自身に
 {\tt sm\_join} が戻って来た場合は、その{\tt sm\_join} は
 廃棄される。現在は、既にsession/editorを持つSMは、他のSMに
 接続することは出来ない。
+<center><img src="fig/many_session_manager.pdf" alt="Session Manager同士の接続"></center>
 ---Session 接続 protocol
 SMに接続したエディタは、自分の既にオープンしたファイルを持って接続する
 {\tt put}と、他のエディタへ空のバッファを接続する{\tt join}の二種類の
 によって、すべてのSMに通知される。このファイルの編集に参加したい場合は、
 まず、Editorを空のバッファの状態でSMに{\tt join}コマンドで接続する。
 すると、{\tt put}と同様に{\tt join}したEditorがすべてのSM上に通知される。
 SMのGUI上の操作{\tt select}により、{\tt put}されたファイルと{\tt join}
 したEditorが結びつけられる。
+<center><img src="fig/sm_join.pdf" alt="join コマンド"></center>
 {\tt select}操作では、{\tt join}したEditorと{\tt put}したエディタを
 探し出す必要がある。そのために、SM木上にSM同士に到達するための
 routing tableを構築している。これは、{\tt sm\_join}時に作成される。
 まず{\tt put}したEditorを探し、見つかったら{\tt select\_ack}を、
 {\tt join}したエディタは空のバッファを持っているので、Session master
 ({\tt put}したEditor)に、必要な編集行を要求する{\tt sync}コマンドを
 session ring に送る。Session master は、次のEditor Command を使って
 必要な行を送信する。
+<center><img src="fig/use_case_put_join_over_sm.pdf" alt="Session Managerを介したエディタの接続"></center>
 ---Editor Command
 Editorのコマンドは、すべて、{\tt insert},{\tt delete} に分解される。
 SM上での混乱を避けるために、Editorが直接SMに送ったユーザが生成した
 受け取った Editor Command をキューに入れておく。
 (2) 戻って来たタイミングで、キュー上のEditor Commandを、eid とCommandの
 順序を基にソートする。
 (3) Editor Command がなくても、他のEditorからCommand を受け取ったら、
 NOP Command を生成して、それが戻って来た時にソートを行なう。
+<center><img src="fig/new_merge.pdf" alt="Session Ring上のREPコマンドの送信"></center>
 この手法では、EditorがN個あるSessionの場合、一つのEditor Commandに対して、N-1
 個のNOP Command が生成される。
 そこで、以下のようなMerge Protocol (C)を導入する。(1) Editor Command
 この時に、ユーザが編集コマンドを割り込ませる可能性がある。
 これを防ぐ一つの方法は、Merge 作業が始まった段階で、ユーザ入力を
 block してやれば良い(a)。もう一つの方法は、ユーザ入力の割り込みが
 あった場合は、その入力込みで、もう一度、ソートを実行すれば良い(b)。
+これはリマージと呼ばれる。
+<center><img src="fig/remerge.pdf" alt="リマージ"></center>
 Merge 作業中には、他のSM/Editorからの入力をblockすることは問題ない。
 それは、もともと非同期で動作しており、遅延は許容されるように
 なっている。
 このように簡単に証明することは出来ない。そこで、
 モデル検査器であるJava PathFinder\cite{}を用いる。
 --Protocol の実装
-Session Manager
+Session Manager はJava 1.5で実装されており、 Ecplise は Java によるPlug-in
+となっている。 Emacs は、従来はCで書いたクライアントを接続していたが、
-Ecplise Plug-in
+今は、すべて Emacs Lisp で書かれている。 Vim は、C で記述されており、
+Merger もCで記述されていたが、今回の実装で取り外された。
-Emacs
+今回の実装では、Editor 側の実装のコストが削減されており、Merge Protocol
-Vim
+部分でCで150行程度が削減されている。Editor 側の実装は、Editor Command を
+{\tt insert, delete} に分解する部分の実装が大半である。
+Editor 側で実装する必要があるのは、表\ref{tb:sync}の機能である。
+\end{table}
+\begin{table}[htdp]
+\caption{Editor 側での実装}
+\begin{center}
+\begin{tabular}{|l|l|}
+\hline
+1 & 編集機能の{\tt user\_insert,user\_detele}への分解と、分解したEditor Command の送信 \\
+\hline
+2 & {\tt join,put} Command のUI部分と、Command の送信 \\
+\hline
+3 & {\tt join,put} Command のUI部分と、Command の送信 \\
+\hline
+4 & {\tt join\_ack,put\_ack} の受け取りとsid,eidの設定 \\
+\hline
+5 & 外部からのEditor Commandの非同期受け取りと実行 \\
+\hline
+6 & {\tt sync} Command を受け取った場合の{\tt user\_insert,user\_detele}の生成
+\hline
+7 & Merge 時のlock (optional) \\
+\hline
+7 & {\tt quit} Command \\
+\hline
+\end{tabular}
+\end{center}
+\label{tb:sync}
+\end{table}%
+ファイルのオープン/セーブなどの機能はREPには含まれていない。Master Editor
+も、それ以外のEditorも任意の時点でのローカルなセーブが可能である。
+版管理なども、REP以外の部分で対応する。
+外部からのEditor Command を受け取った場合のカーソルなどの制御は、規定されて
+いない。移動した場合が便利な場合と、そうでない場合があると思われる。
 --Socket Simulator
-Java Pathfinder による検証
+Java Pathfinder による検証を行なうために、直接、Socketを経由せずに、
+Thread を通して通信を行なうライブラリを作成した。
+このライブラリは、最初、java.nio互換ではなく作成し、Merge Protocol
+(A)及び(B)の動作をJava PathFinder で確認した。編集結果の同一性を
+調べるために、Session 内の Editor のquit プロトコルを実装している。
+まず、 {\tt quit } Command がSessin ring に送られ、各Editorは、
+{\tt quit}を受け取ると、自分のユーザ編集コマンドを停止する。その編集を
+終了した後、{\tt quit}を返す。{\tt quit}を受け取った後も、他の
+Editor からのEditor Commandは来る可能性がある。{\tt quit}を最初に
+送ったEditorに{\tt quit}が戻ると、今度は{\tt quit2}をSession Ring
+に流す。これより後に、ユーザ編集コマンドが来ることはない。Editor は
+自分の待っているEditor Commandのackがすべて来るのを確認してから、
+{\tt quit2}を次へ渡す。{\tt quit2}を渡した後は、Editor Command は
+来ないので、終了して良い。最初のEditorへ{\tt quit2}が戻った時点で、
+すべての編集が終了する。
+この時に、Editor のバッファを比較して、
+すべてのEditorのバッファが同じならば、正しくプロトコルが動いた
+ことになる。これをJava PathFinderで検証を行なう。
+(C)の実装を、実際のSession Manager 上で検証するために、java.nio と
+Thread による通信のシミュレーションを切替えることが可能なライブラリ
+を作成した。実際のSession Manager に対する Java PathFinder での
+実行確認は、計算時間の制約により、まだ、可能とはなっていない。
 --検証とデバッグ
+(A)のプロトコルがEditor 二つで動作すること、及び、(B)のプロトコル
+が複数のEditorで動作することを Java PathFinder で確認することが
+出来た。
+(C)は、実際のSession Managerの実装を含む検証となるので、よりハードルが
+高い。現状では、Java PathFinder での動作確認は出来ていない。
+Java PathFinder でvimやEmacsを含む検証は可能とはなっていないが、
+Sample Editor をJava で実装することにより、Java PathFinderでの
+Merge Protocolの検証が可能となっている。
+実際には、vim やEmacs などのEditor側の実装が正しいかどうかを調べる
+ことも重要である。それは、Merge Protocolを切った状態で、Javaの
+Sample Editor に対する動作を確認することで調べることが出来る。
 --比較
+類似のProject としては、GroupKit \cite{}, Soba Project\cite{} がある。
+vim やEmacs などのOpen source editor の実装を含むのが、REPの特徴
+である。
+また、Java で実装されていて、Session Manager 部分、Editor の改変部分、
+Eclipse plugin のすべてが、LGPLで公開されているのも独自な特徴の
+一つである。
+GroupKit はtcl/tkで記述されており、検証などが困難だが、REPでは、
+Java の部分をJava PathFinder で検証することが可能だと思われる。
+しかし、現状では、まだ、検証までには至っていない。
+GroupKit などで使われているマルチメディア編集の同期は、Masterが
+一つ存在し、それに対するCommandの発行と、MasterからのCommandの
+マルチキャストで実現されている\cite{}。REPでは、マルチキャスト
+ではなく、Session ring によって同期を実現している。Ring は、
+遅く信頼性に欠ける部分があるが、ネットワークに対する負荷が
+軽いと言う特徴がある。(C)のMerge Protocolを使うことにより、
+o(n)のパケットで同期を行なうことが出来る。また、マルチキャスト
+を避けているので、WANなどの遅延が大きい部分に複数のストリーム
+を張る必要がないという特徴がある。
+また、Session Manager 上には、Editor Bufferが存在しないので、
+大きなファイルを編集する場合でも、Session Manager のメモリを
+消費することはない。
+--最後に
+このプロジェクトは、sourceforge を通じて公開\cite{}されており、まだ、
+開発途上となっている。
+残念ながら、実際のSession Manager 上でのJava Pathfinder での検証は
+まだ、出来てはないが、通信ライブラリ上での処理をatomicにするなどの
+工夫で可能になると期待している。

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

comparison rep-verify-sigos.ind @ 3:f1214f4b5933