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

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

--Remote Editing Protocol って?

複数の「既存」のEditorを相互に接続する

    Emacs, Vim, Eclipse など

ずいぶん、ながくやってますが...

まだ、動いてません。

--Remote Editing Protocol の設計方針

Local Editing を阻害しない

接続されたEditorは同等

編集結果は最終的に同一になる

途中の非同期的な差は容認する

ネットワーク遅延に強い

行単位のinsert/delete しか扱わない

    すべての編集はinsert/deleteに分解する

Editorの改変を最小限にする

切断は任意

再接続は、新規接続とする

--構成要素

	Editor

	Session Manager

--Session Manager

Editor はdefaultで、ローカルなSession Manager に接続する

<center><img src="fig/one_session_manager.jpg" alt="Session Managerの導入"></center>

--Protocol の構成

	Session Manager への接続 (sm_join)

	Session への接続 (join,put)

	Editor Command の伝搬 (insert/delete)

	Editor Command の衝突の解消(Merge)

---Session managerの接続protocol

<center><img src="fig/many_session_manager.jpg" alt="Session Manager同士の接続"></center>

---Session 接続 protocol

<center><img src="fig/sm_join.jpg" alt="join コマンド"></center>

<center><img src="fig/use_case_put_join_over_sm.jpg" alt="Session Managerを介したエディタの接続"></center>


---Merge Protocol

編集の衝突を解決する

<center><img src="fig/new_merge.jpg" alt="Session Ring上のREPコマンドの送信"></center>


--Merge をSession Manager 上で行なう

	編集Sessionはring を構成する

	編集の衝突をSession Manager で検出する

	Command と Ack はringをそれぞれ一周する

---Merge のSession Managerへの移動

Merge 作業とEditor上の編集が衝突する場合もある

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

Editor側のlockが可能ならばlockしても良い。(optional)

lock の実装が難しい場合もある。

--Editor 側で実装する必要がある機能

<table border="1">
<tr><td>1 <td> 編集機能の user_insert,user_deteleへの分解
<tr><td>2 <td>分解したEditor Command の送信 
<tr><td>3 <td> join,put Command のUI部分と、Command の送信 
<tr><td>4 <td> join_ack,put_ack の受け取りとsid,eidの設定
<tr><td>5 <td> 外部からのEditor Commandの非同期受け取りと実行 
<tr><td>6 <td> sync Command を受け取った場合の user_insert,user_deteleの生成 
<tr><td>7 <td> Merge 時のlock (optional) 
<tr><td>8 <td>  quit Command 
</table>

--Protocol はかなり複雑

	2つでは大丈夫だが、3つでおかしくなる

	切断のタイミング

--アルゴリズムを決める

	Simulator を作成する

	Simulator から実際の実装に移す

実装するもの自体が多い。Simulator から実装すると2度手間。
    
--モデル検証

	Java PathFinder

を用いて、あらゆるInterleavingを調べることが出来る

	初期化の穴を見つけるのは得意

	少数のコマンドで十分にバグが調べられる

--Java PathFinder の限界

	大きなプログラムを動かすのは難しい

	I/Oが含まれると正しく動作しない

そこで、

	Thread 間通信でSocket通信をsimulationするLibraryを作成した

--Thread/Socketを切替えられる通信ライブラリ

実プログラムで通信を含めて、Java PathFinder で検証可能

通信時にコピーをしないので高速

write 後にコマンドを修正すると問題が出る

初期化時にSocket/Simulationを選択する

--テストプログラムの終了という問題

Java PathFinderで検証する場合はプログラムが終了した方が良い

分散プログラムは終了を自明に検出できない

テストの正しさは終了時に判定するのが簡単


--まとめ

REPのSession Manager のプロトコルを設計し、実装した

Java PathFinder で検証するためのSocket/Thread 互換通信ライブラリを実装した

Java PathFinder で検証するために、状態の数を下げる変更を検討中

まだ、バグが残っているので...