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

done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Mar 2009 12:53:57 +0900
parents f1214f4b5933
children
line wrap: on
line source

-title: Remote Editing Protocol の実装と検証

--author: 与儀健人, 宮城健太, 河野真治

--はじめに

本研究室では、vim、Emacs、Ecpliseを相互接続するプロトコルを提案して来た。
今回は、Session Manager を導入することにより、より単純なユーザインタフェース
を実現するとともに、複雑なプロトコルをSession Manager側に閉じ込めて、
Editor側の実装の手間を軽くすることを提案する。

一方で、プロトコル自体がかなり複雑になったので、プロトコルの正しさ
及び、プロトコル実装の正しさを検証する必要が出て来た。
プロトコル検証では、Java PathFinder\cite{havelund98model}の
有効性が知られているが、それを用いるために、ソケット
通信をThread間の同期で実現するライブラリを作成した。
また、Editor側の実装の正しさの検証及びデバッグのために、
テスト用のEditorを作成した。

--Remote Editing Protocol の設計方針

複数人が同じテキストを共有して編集するプロトコルは、
さまざまなものが提案されているが、汎用エディタに実装
する前堤のプロトコルはほとんどない。Remote Editing Protocol 
では、複数のSession Managerと、リング状のSession の上に
編集コマンドを循環させる方法を取っている。

<center><img src="fig/editor_to_editor2.pdf" alt="REPでの相互接続"></center>

この方法を採用した理由はいくつがある。
集中サーバを用いない\underline{分散実装}が一つの前堤になっている。
Session Manager 自体が分散していて、Session Manager は、
(分離されたMergerを除けば)編集コマンドを中継するだけである。
また、既存のエディタを用いるために、
\underline{localな編集}を妨げない点を重視している。遠隔/共有編集を実現
することによって、本来の編集機能が速度低下などにより損なわれることはない。
一度に大量の通信をすることなどを避け
\underline{Network負荷が軽い}こと。
複雑なコマンド入力などのない\underline{Simple なユーザInterface}。
これらを実現するために\underline{Conflictを非同期に解決}し、
変更の伝播の遅延は容認する。また、
\underline{小人数向け}の共有とする。遅延を容認するために、
\underline{遠距離でも使用可能}となる。また、オープンソースとして実装し、
\underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{bib:xp}
における\underline{Pair Programming}での使用を意識しているので、
\underline{Emacs/vim/Eclipseの相互接続}を重視する。
将来的には、動的な変更を可能とする
\underline{Inter-Application Protocol}として使えるものを
目指している。
プロトコル自体の信頼性を増すために、プロトコル自体の正しさ、及び、
実装の正しさを調べることを可能にする。

--Protocol の構成

ここでは、REPをSession manager(SM), Session manager接続プロトコル、
Session 接続プロトコル、Editor Command、Mergeプロトコル、
MergeのSession Managerへの移動の順に説明する。

---Session managerの導入

従来のREPはエディタ間を直接結んでいたが、その場合は相手の
エディタのホスト名やファイル名を直接入力する必要があった。
これは、ユーザに取って繁雑なだけでなく、個々のエディタでの
実装に複雑なUIを含める必要がある。

Session manager(SM)はエディタの動作するホストに一つあり、エディタ
は自動的に決まったポートを通して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
が決められる。SM同士の接続は木構造(SM木)になるようになっており、
唯一のmaster SMが存在する。

同時に相互に{\tt sm\_join} 
が発行される場合もあるので、リングを避けるために、
{\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 idをACKとして受け取る。editor idは、
session manager id (SM id)を含んでおり、全てのSM上でユニークとなる。

{\tt put}したファイルを持つエディタは、そのsessionのmasterとなる。
ファイルを共有するeditor群をsession と呼ぶ。session には、
SM id を含む session id が割り振られ、全てのSM上
でユニークとなる。

ユニークな SM id を使うので、editor id/sesison id はmaster SMに問い合わせる
ことなく生成が可能となる。

{\tt put}されたファイルはSM木を{\tt put}コマンドで遡り、{\tt put\_ack}
によって、すべての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}を、
session ring を構築しながら{\tt join}したEditorを探す。見つかったら
{\tt join\_ack}がEditorに返される。
この時に、必要があれば、{\tt join}側、{\tt put}側の認証を行なう。

{\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 {\tt user\_inert, user\_delete}と SM経由で送られた他のEditor Command は異なる
コマンドとして扱っている。

Editor は複数のsession を持つことも可能であるが、一つのEditor
が同じSessionに複数回{\tt join}すると、Editorの通信経路とEditor
id が対応しなくなる。問題はないが、実装はより複雑となる。

次のMerge Protocolでは、SM上でEditorのコマンドのundoを計算する
必要があるので、{\tt  user\_delete}には、削除した行の内容が
付加されてSMに送られる。したがって、{\tt  user\_delete}と
{\tt  user\_insert}と見掛け上対称となる。

全文置換なども{\tt user\_inert, user\_delete}に分解する必要が
あり、その分解はEditorによって行なわれる。REPは歴史的理由で行指向の
プロトコルであり、行指向でないEditorでも行番号を付加する
必要がある。

{\tt sync}に対しては、要求された行に対して、
{\tt delete, insert}を順に送ることで、{\tt join}したEditorに
行を転送する。特別なバッファ転送コマンドはない。

置換を特別扱いすることによるコマンド短縮の利点があるように
思えるが、SMではundoを生成する必要があるので、変更前の行と
変更後の行を送る必要があり、
{\tt delete, insert}を順に送る場合との差は無視できる。

---Merge Protocol

一つのSessionの上で、複数のEditorが同時に編集を行なった場合には、
その結果は、最終的に、Session 上で同じになる必要がある。

REPでは、二つのEditorの場合の編集の衝突の解決を行なう
手法を提案して来た。この方法(Merge Protocol (A))では自分のEditor Commandを
相手に送り、戻って来るまでのEditor Commandをキューに入れておく。
他のEditorのCommandを受け取った時には、その
キューと、そのCommandの可換性を調べて、キューを変更する\cite{kono04g}。
しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。

そこで、以下のようなMerge Protocol (B)を導入する。(1) Editor Command
をSession Ring 上に流し、それが戻って来るまでに、他のEditorから
受け取った 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
をSession Ring 上に流し、それが戻って来るまでに、他のEditorから
受け取った Editor Command をキューに入れておく。
(2) 戻って来たタイミングで、キュー上のEditor Commandを、eid とCommandの
順序を基にソートする。
(3) 他のEditorにソートのタイミングを与えるために、Editor Command の
ack を、もう一周させる。
(4) 他のEditorのCommandを受け取ってから、ack が来るまでのCommandをキューに
入れておき、ack が来たら、eid とCommandの順序を基にソートする。

Editor には、ソートした編集結果になるように、それまで行なった編集をUndo
して、ソートした編集結果を適用する。

---Merge のSession Managerへの移動

Merge Protocol は、かなり複雑であり、すべてのEditor実装に対して
実装する必要がある。我々のターゲット(Vim, Emacs, Eclipse)は、
すべて異なる言語(C,Emacs Lisp,Java)で実装されており、そのすべてで、
複雑なプロトコルを実装するのは不可能ではないが、コストがかかる。

今回は、SMが一つのEditorに対して必ず存在するので、Merge Procotol
をSMに実装すると、SMの実装言語(Java)に実装するので十分になる。
しかし、Merge Protocol は編集バッファに対して複雑な操作をするので、
それをEditor Command を通して実装する必要がある。

まず、Editor Command がUndo(取消し)可能でなければならない。
このために、{\tt user\_delete} Command に削除した行の内容を
付加することにした。

次に、SMがMerge Protocolでソートした編集結果を適用した結果は、
(可能な最適化をした)Editor Command 列でEditorに反映する必要がある。
この時に、ユーザが編集コマンドを割り込ませる可能性がある。

これを防ぐ一つの方法は、Merge 作業が始まった段階で、ユーザ入力を
block してやれば良い(a)。もう一つの方法は、ユーザ入力の割り込みが
あった場合は、その入力込みで、もう一度、ソートを実行すれば良い(b)。
これはリマージと呼ばれる。

<center><img src="fig/reMerge.pdf" alt="リマージ"></center>

Merge 作業中には、他のSM/Editorからの入力をblockすることは問題ない。
それは、もともと非同期で動作しており、遅延は許容されるように
なっている。

ユーザ入力のlock(a)は、エディタの実装に依存していて、実装はさまざまで
ある。また、REP設計の一つの目標であるlocalな編集を妨げないという
点では問題が残る。(b) は、Merge Protocol の実装が繁雑になるが、
ユーザの入力を妨げることはない。また、エディタのlockを実装しなくて
すむ。(a),(b)はお互いに干渉しないので、エディタのlockの実装は
REPを実装する時の選択肢の一つとなる。lock がある方が大量の変更(コピー
ペースト)がある場合にスムースな動作が期待できる。


--Protocol の正しさ

Merge Protocol の正しさの証明は、Protocol自体の正しさと、
Protocolの実装を含めた正しさの二種類の正しさを示す必要がある。

ここでは、(A)のProtocolの正しさを示す。Editor $0..n$ が、
それぞれ、編集コマンド$C_{ij}$ (Editor $i$の$j$番目のコマンド,$j$は0から)を
入力したとする。このコマンドは、Session ring を巡回する。
巡回するたびに、各Editor $k$が{\tt NOP} Command $N_{kx}$を、その
コマンドの前に付加する。
% (A)では自分が既にCommandを送っていれば{\tt NOP}を付加する必要は
% ないが、ここでは、必ず付加することにする。
$x$は、コマンドの順序である。
% $C_{ij}$の$j$は、{\tt NOP}を含めた番号に付け換える。

Editor $m$では、
\[  C_{m0} C_{x0} N_{00} .... N_{yz} \]
などのコマンド列が実行されることになる。これを$C/N$の
区別のないコマンド記号($E_{ij}$)で置き換えよう。
\[  E_{m0} E_{x0} E_{00} .... E_{yz} \]
NOPの付加手順から、
他のEditorが送ったCommandには、その前の他のEditorからのCommandを
受け取った後の、
自分が送ったCommand(0以上の複数個)
または、{\tt NOP}
が必ず対応している。
対応するCommandとは、Session ring 上で同時に実行されたと考えられる
Command の集合と考えて良い。
Command はSession ring  を一周するので、すべての
Editor が同じCommandの集合を受け取っている。

ここで、対応したCommandの集まり毎に列を分割し、
Editor iの
その集まりを集合と
みなし$S_{ij}$ とする。この集合の列を$Z_i$とする。
\[  Z_i = S_{i0} S_{i1} .... S_{in} \]
定義から隣同士の$S_{ij}$には、
対応したCommandが含まれることはない。

この集合列$Z$は、すべてのEditorで同一となる。
[証明]
Editor $i$とEditor $j$で、$S_{ik}$と、$j$の$S_{jk}$が異なっている
としよう。あるCommand $E_s$があって、
$E_s \in S_{ik}$であって$E_s \in S_{jk}$でない。
しかし、$E_s$
はsession ringを一周しているので、$S_{ik}$と$S_{jk}$の両方に
含まれているか、隣同士にあるはずである。両方に含まれていると
すると仮定と矛盾するので、隣同士になるはずである。しかし、隣同士で
あれば、Command の分割の方法に矛盾する。[証明終り]

従って、$S_i$をEditor idとCommand順序によってソートしてやれば、
すべてのEditorで、同一なCommand列を得ることが出来る。
ソートのタイミングは、対応するコマンドがすべて自分に到着した時点である。
自分の送った新しいコマンド、または、新しい{\tt NOP}が
来たことによって、その一つ前までが対応しているものだということがわかる
ので、その時点でソートしてやれば良い。従って、Merge Protocolにより、
すべてのEditorで同一の編集結果が得られることがわかった。

(B)では、{\tt NOP}の挿入の代わりに{\tt ack}を、もう一周させている。
{\tt ack} が来た時点で、対応するCommandの集合が確定する。あるいは、
仮想的に{\tt NOP}を挿入したと考えると、その{\tt NOP}は、{\tt ack}
の前に挿入されていると考えて良い。従って、(A)と同じように集合列$Z$
を、すべてのEditorで同一となるように決めることが出来る。

プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、
このように簡単に証明することは出来ない。そこで、
モデル検査器であるJava PathFinder\cite{havelund98model}を用いる。

--Protocol の実装

Session Manager はJava 1.5で実装されており、 Ecplise は Java によるPlug-in
となっている。 Emacs は、従来はCで書いたクライアントを接続していたが、
今は、すべて Emacs Lisp で書かれている。 Vim は、C で記述されており、
Merger もCで記述されていたが、今回の実装で取り外された。

今回の実装では、Editor 側の実装のコストが削減されており、Merge Protocol
部分でCで150行程度が削減されている。Editor 側の実装は、Editor Command を
{\tt insert, delete} に分解する部分の実装が大半である。

Editor 側で実装する必要があるのは、表\ref{tb:sync}の機能である。
\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 による検証を行なうために、直接、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{bib:groupkit}, Soba Project\cite{bib:soba} がある。
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{bib:ellis}。REPでは、マルチキャスト
ではなく、Session ring によって同期を実現している。Ring は、
遅く信頼性に欠ける部分があるが、ネットワークに対する負荷が
軽いと言う特徴がある。(C)のMerge Protocolを使うことにより、
o(n)のパケットで同期を行なうことが出来る。また、マルチキャスト
を避けているので、WANなどの遅延が大きい部分に複数のストリーム
を張る必要がないという特徴がある。

また、Session Manager 上には、Editor Bufferが存在しないので、
大きなファイルを編集する場合でも、Session Manager のメモリを
消費することはない。

--最後に

このプロジェクトは、sourceforge を通じて公開\cite{rep-sourceforge}されており、まだ、
開発途上となっている。

残念ながら、実際のSession Manager 上でのJava Pathfinder での検証は
まだ、出来てはないが、通信ライブラリ上での処理をatomicにするなどの
工夫で可能になると期待している。