Mercurial > hg > Papers > 2009 > rep-verify-sigos
diff 6.tex @ 5:34bfeb51e287
add section tex file, Makefile
author | gongo@gendarme.local |
---|---|
date | Sat, 28 Mar 2009 16:26:43 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/6.tex Sat Mar 28 16:26:43 2009 +0900 @@ -0,0 +1,30 @@ +\section{ Socket Simulator} + +Java Pathfinder による検証を行なうために、直接、Socketを経由せずに、 +Thread を通して通信を行なうライブラリを作成した。 + +このライブラリは、最初、java.nio互換ではなく作成し、Merge Protocol +(A)及び(B)の動作をJava PathFinder で確認した。編集結果の同一性を +調べるために、Session 内の Editor のquit プロトコルを実装している。 + +まず、 {\tt quit } Command がSessin ring に送られ、各Editorは、 +{\tt quit}を受け取ると、自分のユーザ編集コマンドを停止する。その編集を +終了した後、{\tt quit}を返す。{\tt quit}を受け取った後も、他の +Editor からのEditor Commandは来る可能性がある。{\tt quit}を最初に +送ったEditorに{\tt quit}が戻ると、今度は{\tt quit2}をSession Ring +に流す。これより後に、ユーザ編集コマンドが来ることはない。Editor は +自分の待っているEditor Commandのackがすべて来るのを確認してから、 +{\tt quit2}を次へ渡す。{\tt quit2}を渡した後は、Editor Command は +来ないので、終了して良い。最初のEditorへ{\tt quit2}が戻った時点で、 +すべての編集が終了する。 + +この時に、Editor のバッファを比較して、 +すべてのEditorのバッファが同じならば、正しくプロトコルが動いた +ことになる。これをJava PathFinderで検証を行なう。 + + +(C)の実装を、実際のSession Manager 上で検証するために、java.nio と +Thread による通信のシミュレーションを切替えることが可能なライブラリ +を作成した。実際のSession Manager に対する Java PathFinder での +実行確認は、計算時間の制約により、まだ、可能とはなっていない。 +