# HG changeset patch # User e155702 # Date 1550710007 -32400 # Node ID c9142e57399fb482c2a7fd5e41487fece573e4c3 # Parent e2ec8297e712bc1b78c1ae10cb9d14b2bbaa86ce uodate maintex diff -r e2ec8297e712 -r c9142e57399f final_main/chapter2.tex --- a/final_main/chapter2.tex Wed Feb 20 14:36:21 2019 +0900 +++ b/final_main/chapter2.tex Thu Feb 21 09:46:47 2019 +0900 @@ -105,8 +105,30 @@ TreeVNC の木構造のネットワークトポロジーは Root Node が持っている nodeList で管理している。 Node の接続が切れた場合、Root Node に切断を知らせる必要がある。この時 LOST\_CHILD というメッセージで Node の切断を検知・木の再構成を行う。LOST\_CHILD の検出方法には MulticastQueue を使用している(一定期間 MulticastQueue から画像データが取得されない場合、 MemoryOverFlow を回避するために Timeout スレッドが用意されており、これを検知した場合 Node の接続が切れたと判断する)。 + \section{ZRLEE} +TreeVNC では、ZRLEE というエンコード方法でデータの圧縮を行う。ZRLEE は RFB プロトコルで使用できる ZRLE というエンコード方法を元に生成されている。 +ZRLE は Zlib で圧縮されたデータとそのデータのバイト数がヘッダーとして付属して送られて来る。Zlib は java.util.zip.deflater と java.util.zip.inflater でエンコード・デコードが行える。 +しかし、java.util.zip.deflater はデコードに必要な辞書を書き出すことができない(図\ref{fig:zre})。従って、エンコードされたデータを途中から呼ぶと正しく解凍できない。 + +ZRLEE は1度 Root Node で受け取った ZRLE のデータを unzip し、データを update rectangle という画面ごとのデータに辞書を付けて zip し直すことで初めからデータを呼んでいなくてもデコードできるようにしている(図\ref{fig:zrlee})。1度 ZRLEE に変換してしまえば子 Node はそのデータを流すだけで良い。ただし、deflater と inflater では前回までの通信で得た辞書をクリアしないといけないため、Root Node と Node 側では毎回新しく作成する必要がある。 + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/zre-crop.pdf}} + \end{center} + \caption{ZRE の問題点} + \label{fig:zre} +\end{figure} + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/zrlee-crop.pdf}} + \end{center} + \caption{ZRLEE} + \label{fig:zrlee} +\end{figure} \section{ShereScreen} @@ -114,3 +136,17 @@ ShareScreen 実行後、Root Node に対し SERVER\_CHANGE\_REQUEST というメッセージが送信される。このメッセージには ShereScreen ボタンを押した Node の番号やディスプレイの情報が付加されている。メッセージを受け取った Root Node は配信を希望している Node の VNC サーバーと通信を行い、切り替え作業に入る。 + +\section{ネットワーク複数時の接続} +TreeVNC は Root Node が複数のネットワークに接続している場合、(図\ref{fig:networktree})の様にネットワーク別に木構造を形成する。 + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/networktree-crop.pdf}} + \end{center} + \caption{multinetworktree} + \label{fig:networktree} +\end{figure} + +TreeVNC は Root Node が TreeManager というオブジェクトを持っている。TreeM- anager は TreeVNC の接続部分を管理している。TreeManager では木構造を管理する nodeList が生成される。この nodeList を元に、新しい Node の接続や、切断検出時の接 続の切り替え等を行う。 +Root Node の保持しているネットワーク毎に TreeManager を生成する。新しい Node が接続してきた際、 interfaces から Node のネットワークと一致する TreeManager を取 得し、 Node 接続の処理を任せる。 diff -r e2ec8297e712 -r c9142e57399f final_main/chapter5.tex --- a/final_main/chapter5.tex Wed Feb 20 14:36:21 2019 +0900 +++ b/final_main/chapter5.tex Thu Feb 21 09:46:47 2019 +0900 @@ -1,139 +1,1 @@ -\chapter{Agda による CbC の証明} - -前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード -を Agda にマッピングし等価なコードを生成できることを示した。 -本章では前章で生成した Interface の Stack や Tree のコードを使い Agda で -Interface を経由したコードでの証明が可能であることを示す。 - -% Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。 -% ↑ 上は Tree のコードが証明できないことを示して、その次の章に Hoare Logic でこ -% んな感じにするとできるのでは？っていう感じにしよ - -\section{Agda による Interface 部分を含めた Stack の部分的な証明} -\label{src:agda-interface-stack} - -% Stack の仕様記述 -ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。 - -Stack の処理として様々な性質が存在する。例えば、 - -\begin{itemize} - \item Stack に push した値は存在する - \item Stack に push した値は取り出すことができる - \item Stack に push した値を pop した時、その値は Stack から消える - \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない - \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する -\end{itemize} - -などの性質がある。 - -本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前 -に入れた値と一致する」という性質を証明する。 - - -% この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ -% ものが受け取れることを 証明している。 - -まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state} -の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー -ド~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を -2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい -る。 - - \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced} - -% Agda でも継続を使った書き方で Interface 部分の実装を示した。 - -この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー -タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が -Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として -型に書かれている。 - -% この辺ちょっと怪しい感じ -この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと -めて refl で推論が通る。 -これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも -のを受け取れることが証明できた。 - - -% \lstinputlisting[label=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced} - -\section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題} -ここでは Binary Tree の性質の一部に対して証明を行う。 -Binary Tree の性質として挙げられるのは次のようなものである -% 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる - -\begin{itemize} - \item Tree に対して Node を Put することができる。 - \item Tree に Put された Node は Delete されるまでなくならない。 - \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。 - \item どのような状態の Tree に値を put しても Node と子の関係は保たれる - \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。 -\end{itemize} - -ここで証明する性質は - -${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。 - -\lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証 -明]{src/AgdaTreeProof.agda.replaced} - -この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree -に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの -である。 - -しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した -Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、 -key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が -あった。今回この証明では Put した Node と Get した -Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合 -同であることを示すことが困難であった。 - -今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を -行おうと考えている。 - -\section{Hoare Logic} -\label{hoare-logic} - -Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正 -しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition) -、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \ C \ \{Q\}$ のように考えたとき、 -プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。 - -\begin{figure}[htpb] - \begin{center} - \scalebox{0.6}[0.6]{\includegraphics{fig/hoare-logic.pdf}} - \end{center} - \caption{hoare logicの流れ} - \label{fig:hoare} -\end{figure} - - -このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい -動きをすることを証明することができる。 - -この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表 -\ref{fig:cbc-hoare} のように表せるのではないか考えている。 - -\begin{figure}[htpb] - \begin{center} - \scalebox{0.8}[0.8]{\includegraphics{fig/cbc-hoare.pdf}} - \end{center} - \caption{cbc と hoare logic} - \label{fig:cbc-hoare} -\end{figure} - -この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると -Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が -CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて -いる。 - -今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に -当てはめ、幾つかの実装を証明していく。 - -% Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。 -% 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。 -%% -% 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導 -% 入した。 -%% \ No newline at end of file +\chapter{} diff -r e2ec8297e712 -r c9142e57399f final_main/main.pdf Binary file final_main/main.pdf has changed diff -r e2ec8297e712 -r c9142e57399f final_pre/main.tex --- a/final_pre/main.tex Wed Feb 20 14:36:21 2019 +0900 +++ b/final_pre/main.tex Thu Feb 21 09:46:47 2019 +0900 @@ -94,18 +94,13 @@ \begin{center} \includegraphics[scale=0.4]{images/tiling-crop.pdf} \end{center} - \caption{データ解凍時の画面の分割イメージ} + \caption{データ圧縮時の画面の分割イメージ} \label{fig:tiling} \end{figure} しかし、無線接続では有線接続よりも送信できるデータ量が少ないため、さらに分割する必要がある。 そこでデータを再分割する手法として Blocking を実装した。 -FrameBufferUpdate で受け取った部分を更新 -更新部分の最大値を保持 -幅 width * bytePerPixel (1ピクセルあたりのデータ量) ずつ deflate していき、書き込み用に用意した関数の残り値を超える直前に関数に全て書き込み、header などを添付して他のクラスに渡す -Indexをインクリメントしていき最大値になったら停止 - Blocking 実装後 VNCServer とクライアントの接続を行ったところ、十分な転送速度を確認できた。 %実演?結果出して diff -r e2ec8297e712 -r c9142e57399f slide/slide.html --- a/slide/slide.html Wed Feb 20 14:36:21 2019 +0900 +++ b/slide/slide.html Thu Feb 21 09:46:47 2019 +0900 @@ -86,7 +86,7 @@ diff -r e2ec8297e712 -r c9142e57399f slide/slide.pdf.html --- a/slide/slide.pdf.html Wed Feb 20 14:36:21 2019 +0900 +++ b/slide/slide.pdf.html Thu Feb 21 09:46:47 2019 +0900 @@ -70,7 +70,7 @@