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