--- a/rep-verify-sigos.ind	Sat Mar 21 22:34:51 2009 +0900
+++ b/rep-verify-sigos.ind	Thu Mar 26 03:33:07 2009 +0900
@@ -2,47 +2,293 @@
 
 --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_join
+SM同士の接続は、{\tt sm\_join}コマンドをSMに送ることによる。
+接続により、接続したSM間でuniqueな session manager id
+が決められる。SM同士の接続は木構造(SM木)になるようになっており、
+唯一のmaster SMが存在する。
 
-session manager id
+同時に相互に{\tt sm\_join} 
+が発行される場合もあるので、リングを避けるために、
+{\tt sm\_join} はmaster SMまで転送される。自分自身に
+{\tt sm\_join} が戻って来た場合は、その{\tt sm\_join} は
+廃棄される。現在は、既にsession/editorを持つSMは、他のSMに
+接続することは出来ない。
 
 ---Session 接続 protocol
 
-session id
+SMに接続したエディタは、自分の既にオープンしたファイルを持って接続する
+{\tt put}と、他のエディタへ空のバッファを接続する{\tt join}の二種類の
+接続を行なう。
+
+接続が行なわれると、SMからeditor idをACKとして受け取る。editor idは、
+session manager id (SM id)を含んでおり、全てのSM上でユニークとなる。
 
-editor id
+{\tt put}したファイルを持つエディタは、そのsessionのmasterとなる。
+ファイルを共有するeditor群をsession と呼ぶ。session には、
+SM id を含む session id が割り振られ、全てのSM上
+でユニークとなる。
+
+ユニークな SM id を使うので、editor id/sesison id はmaster SMに問い合わせる
+ことなく生成が可能となる。
 
-join/put
+{\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が結びつけられる。
 
-select
+{\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
 
-point to point
+一つのSessionの上で、複数のEditorが同時に編集を行なった場合には、
+その結果は、最終的に、Session 上で同じになる必要がある。
+
+REPでは、二つのEditorの場合の編集の衝突の解決を行なう
+手法を提案して来た。この方法(Merge Protocol (A))では自分のEditor Commandを
+相手に送り、戻って来るまでのEditor Commandをキューに入れておく。
+他のEditorのCommandを受け取った時には、その
+キューと、そのCommandの可換性を調べて、キューを変更する\cite{}。
+しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。
 
-merge ring ( nop の挿入)
+そこで、以下のような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 ring ( ack の導入)
+そこで、以下のような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時の衝突解消
+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 に削除した行の内容を
+付加することにした。
 
-Editor のlock
+次に、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 の正しさの証明
+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 の実装