Mercurial > hg > Papers > 2009 > rep-verify-sigos
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 での検証は