diff 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 diff
--- a/rep-verify-sigos.ind	Thu Mar 26 10:31:47 2009 +0900
+++ b/rep-verify-sigos.ind	Thu Mar 26 12:53:57 2009 +0900
@@ -11,7 +11,7 @@
 
 一方で、プロトコル自体がかなり複雑になったので、プロトコルの正しさ
 及び、プロトコル実装の正しさを検証する必要が出て来た。
-プロトコル検証では、Java PathFinder\cite{javapathfinder}の
+プロトコル検証では、Java PathFinder\cite{havelund98model}の
 有効性が知られているが、それを用いるために、ソケット
 通信をThread間の同期で実現するライブラリを作成した。
 また、Editor側の実装の正しさの検証及びデバッグのために、
@@ -41,7 +41,7 @@
 変更の伝播の遅延は容認する。また、
 \underline{小人数向け}の共有とする。遅延を容認するために、
 \underline{遠距離でも使用可能}となる。また、オープンソースとして実装し、
-\underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{xp}
+\underline{教育用途}に向いている。特に、XP (eXtreme Programming) \cite{bib:xp}
 における\underline{Pair Programming}での使用を意識しているので、
 \underline{Emacs/vim/Eclipseの相互接続}を重視する。
 将来的には、動的な変更を可能とする
@@ -141,7 +141,7 @@
 付加されてSMに送られる。したがって、{\tt  user\_delete}と
 {\tt  user\_insert}と見掛け上対称となる。
 
-全文置換なども{\tt user\_inert, user_delete}に分解する必要が
+全文置換なども{\tt user\_inert, user\_delete}に分解する必要が
 あり、その分解はEditorによって行なわれる。REPは歴史的理由で行指向の
 プロトコルであり、行指向でないEditorでも行番号を付加する
 必要がある。
@@ -164,7 +164,7 @@
 手法を提案して来た。この方法(Merge Protocol (A))では自分のEditor Commandを
 相手に送り、戻って来るまでのEditor Commandをキューに入れておく。
 他のEditorのCommandを受け取った時には、その
-キューと、そのCommandの可換性を調べて、キューを変更する\cite{}。
+キューと、そのCommandの可換性を調べて、キューを変更する\cite{kono04g}。
 しかし、この方法は、三つ以上のEditorの場合はうまく動作しない。
 
 そこで、以下のようなMerge Protocol (B)を導入する。(1) Editor Command
@@ -218,7 +218,7 @@
 あった場合は、その入力込みで、もう一度、ソートを実行すれば良い(b)。
 これはリマージと呼ばれる。
 
-<center><img src="fig/remerge.pdf" alt="リマージ"></center>
+<center><img src="fig/reMerge.pdf" alt="リマージ"></center>
 
 Merge 作業中には、他のSM/Editorからの入力をblockすることは問題ない。
 それは、もともと非同期で動作しており、遅延は許容されるように
@@ -251,7 +251,7 @@
 Editor $m$では、
 \[  C_{m0} C_{x0} N_{00} .... N_{yz} \]
 などのコマンド列が実行されることになる。これを$C/N$の
-区別のないコマンド記号(E_{ij})で置き換えよう。
+区別のないコマンド記号($E_{ij}$)で置き換えよう。
 \[  E_{m0} E_{x0} E_{00} .... E_{yz} \]
 NOPの付加手順から、
 他のEditorが送ったCommandには、その前の他のEditorからのCommandを
@@ -299,7 +299,7 @@
 
 プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、
 このように簡単に証明することは出来ない。そこで、
-モデル検査器であるJava PathFinder\cite{}を用いる。
+モデル検査器であるJava PathFinder\cite{havelund98model}を用いる。
 
 --Protocol の実装
 
@@ -313,7 +313,6 @@
 {\tt insert, delete} に分解する部分の実装が大半である。
 
 Editor 側で実装する必要があるのは、表\ref{tb:sync}の機能である。
-\end{table}
 \begin{table}[htdp]
 \caption{Editor 側での実装}
 \begin{center}
@@ -329,7 +328,7 @@
 \hline
 5 & 外部からのEditor Commandの非同期受け取りと実行 \\
 \hline
-6 & {\tt sync} Command を受け取った場合の{\tt user\_insert,user\_detele}の生成
+6 & {\tt sync} Command を受け取った場合の{\tt user\_insert,user\_detele}の生成 \\
 \hline
 7 & Merge 時のlock (optional) \\
 \hline
@@ -397,7 +396,7 @@
 
 --比較
 
-類似のProject としては、GroupKit \cite{}, Soba Project\cite{} がある。
+類似のProject としては、GroupKit \cite{bib:groupkit}, Soba Project\cite{bib:soba} がある。
 vim やEmacs などのOpen source editor の実装を含むのが、REPの特徴
 である。
 
@@ -411,7 +410,7 @@
 
 GroupKit などで使われているマルチメディア編集の同期は、Masterが
 一つ存在し、それに対するCommandの発行と、MasterからのCommandの
-マルチキャストで実現されている\cite{}。REPでは、マルチキャスト
+マルチキャストで実現されている\cite{bib:ellis}。REPでは、マルチキャスト
 ではなく、Session ring によって同期を実現している。Ring は、
 遅く信頼性に欠ける部分があるが、ネットワークに対する負荷が
 軽いと言う特徴がある。(C)のMerge Protocolを使うことにより、
@@ -425,7 +424,7 @@
 
 --最後に
 
-このプロジェクトは、sourceforge を通じて公開\cite{}されており、まだ、
+このプロジェクトは、sourceforge を通じて公開\cite{rep-sourceforge}されており、まだ、
 開発途上となっている。
 
 残念ながら、実際のSession Manager 上でのJava Pathfinder での検証は