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

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

--はじめに

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

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

--Remote Editing Protocol の設計方針

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

この方法を採用した理由はいくつがある。
集中サーバを用いない\underline{分散実装}が一つの前堤になっている。
Session Manager 自体が分散していて、Session Manager は、
(分離されたMergerを除けば)編集コマンドを中継するだけである。
また、既存のエディタを用いるために、
\underline{localな編集}を妨げない点を重視している。遠隔/共有編集を実現
することによって、本来の編集機能が速度低下などにより損なわれることはない。
一度に大量の通信をすることなどを避け
\underline{Network負荷が軽い}こと。
複雑なコマンド入力などのない\underline{Simple なユーザInterface}。
これらを実現するために\underline{Conflictを非同期に解決}し、
変更の伝播の遅延は容認する。また、
\underline{小人数向け}の共有とする。遅延を容認するために、
\underline{遠距離でも使用可能}となる。また、オープンソースとして実装し、
\underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{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)する。

---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に
接続することは出来ない。

---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が結びつけられる。

{\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 を使って
必要な行を送信する。

---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{}。
しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。

そこで、以下のようなMerge Protocol (B)を導入する。(1) Editor Command
をSession Ring 上に流し、それが戻って来るまでに、他のEditorから
受け取った Editor Command をキューに入れておく。
(2) 戻って来たタイミングで、キュー上のEditor Commandを、eid とCommandの
順序を基にソートする。
(3) Editor Command がなくても、他のEditorからCommand を受け取ったら、
NOP Command を生成して、それが戻って来た時にソートを行なう。

この手法では、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)。

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{}を用いる。

--Protocol の実装

Session Manager

Ecplise Plug-in

Emacs 

Vim

--Socket Simulator

Java Pathfinder による検証

--検証とデバッグ

--比較