--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presentation/fig	Fri Apr 24 07:50:06 2009 +0900
@@ -0,0 +1,1 @@
+../fig
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presentation/rep-verify-sigos.ind	Fri Apr 24 07:50:06 2009 +0900
@@ -0,0 +1,183 @@
+-title: Remote Editing Protocol の実装と検証
+
+--author: 与儀健人, 宮城健太, 河野真治
+
+--はじめに
+
+
+--Remote Editing Protocol の設計方針
+
+複数の「既存」のEditorを相互に接続する
+
+    Emacs, Vim, Eclipse など
+
+Local Editing を阻害しない
+
+接続されたEditorは同等
+
+編集結果は最終的に同一になる
+
+途中の非同期的な差は容認する
+
+ネットワーク遅延に強い
+
+行単位のinsert/delete しか扱わない
+
+    すべての編集はinsert/deleteに分解する
+
+Editorの改変を最小限にする
+
+切断は任意
+
+再接続は、新規接続とする
+
+--構成要素
+
+	Editor
+
+	Session Manager
+
+--Protocol の構成
+
+	Session Manager への接続 (sm_join)
+
+	Session への接続 (join,put)
+
+	Editor Command の伝搬 (insert/delete)
+
+	Editor Command の衝突の解消(Merge)
+
+--Merge をSession Manager 上で行なう
+
+	編集Sessionはring を構成する
+
+	編集の衝突をSession Manager で検出する
+
+	Command と Ack はringをそれぞれ一周する
+
+--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で検証する場合はプログラムが終了した方が良い
+
+分散プログラムは終了を自明に検出できない
+
+テストの正しさは終了時に判定するのが簡単
+
+---Session managerの導入
+
+<center><img src="fig/one_session_manager.pdf" alt="Session Managerの導入"></center>
+
+---Session managerの接続protocol
+
+<center><img src="fig/many_session_manager.pdf" alt="Session Manager同士の接続"></center>
+
+---Session 接続 protocol
+
+<center><img src="fig/sm_join.pdf" alt="join コマンド"></center>
+
+<center><img src="fig/use_case_put_join_over_sm.pdf" alt="Session Managerを介したエディタの接続"></center>
+
+---Editor Command
+
+
+---Merge Protocol
+
+
+<center><img src="fig/new_merge.pdf" alt="Session Ring上のREPコマンドの送信"></center>
+
+
+---Merge のSession Managerへの移動
+
+
+<center><img src="fig/reMerge.pdf" alt="リマージ"></center>
+
+
+--Protocol の正しさ
+
+
+--Protocol の実装
+
+
+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}%
+
+
+--Socket Simulator
+
+
+--検証とデバッグ
+
+
+--比較
+
+
+--最後に
+