Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Thu Jul 07 17:22:35 2016 +0900
+++ b/paper/vmpcbc.tex	Thu Jul 07 18:39:23 2016 +0900
@@ -38,32 +38,6 @@
 
 \begin{document}
 
-% ipsjpro
-%     cbmc でできなかった理由とかも書く
-%         実際はフェアじゃないし
-%
-% --- たけだくんから ---
-% Attonさん
-%
-% Treeの大きさがどれくらいなのかという図
-% CBCで書かれたRed black Treeも書いた方がいい
-%
-% なぜswitchを入れている？
-% セグフォした時に前のコードがわからない
-% ー＞デバッグ用のコード
-%
-% 次のためにみたいなので
-% const struct Node* node = akashaInfo -> akashaNode-> Node;の go toの部分
-%
-% なぜcbcで苦労して書くのか？
-% toy program的なのを書きたい
-%
-% パルスさんの書いたコンピテーション部分を持ってく
-% kkbさんの修論があればいいなぁ
-%
-% ポインターの計算とかはAkashaにはない
-% cbmcであればこういう風に書けば検証できる
-
 \title{Continuation based C を用いたプログラムの検証手法}
 \etitle{Verification method of programs using Continuation based C}
 
@@ -123,9 +97,8 @@
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
 
 \section{Code SegmentとData Segment}
-% どうしてcs/dsなのかのストーリ＝とか
-動作するコードを検証しやすいよう、本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
-Code Segmentとは処理の単位であり、ループを含まない単純な処理のみを行なう。
+動作するコードを検証しやすい単位で記述するために本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
+Code Segmentとは処理の単位であり、ループを含まないような単純な処理のみを行なう。
 プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。
 Code Segment間における値の受け渡しには、Data Segmentというデータの単位で行なう。
 なお、接続されたCode Segmentには依存関係が発生するが、依存関係が無いCode Segmentは並列に実行することが可能である。
@@ -156,12 +129,13 @@
 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
-Code SegmentとData Segmentを用いたプログラミングスタイルで記述するとして Continuation based C\cite{cite:cbc-clang} 言語を作成した。
+Code SegmentとData Segmentを用いたプログラミングスタイルで記述する言語として Continuation based C\cite{cite:cbc-clang} を作成した。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えたものである。
 Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。
 軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。
-なお、C言語の資産を利用するために通常の関数呼び出しを行なうことも可能である。
+なお、C言語の資産を利用するために関数呼び出しを行なうことも可能である。
+また、Code Segment のみが導入されたCbCで検証を行った例として Dining Philosophers Problem のデッドロック検知\cite{cite:dpp}がある。
 
 % {{{ Code Segment の接続(10加算して2倍する)
 \begin{table}
@@ -199,7 +173,7 @@
         int x;
     } count;
     struct Port {
-        unsigned int port;
+        int port;
     } port;
 };
 \end{lstlisting}
@@ -252,7 +226,7 @@
 // Meta Data Segment
 struct Context {
     union Data *data;  // Data Segment
-    unsigned int gotoCount; /* メタ計算に必要なデータ */
+    unsigned int gotoCount; // メタ計算に必要なデータ
     unsigned int stepOfAddTen;
 };
 
@@ -264,7 +238,7 @@
     /* 接続時に行なうメタ計算を記述 */
     switch (next) {
         case AddTen:
-            /* 特定のCode Segmentへのメタ計算 */
+            // 特定のCode Segmentへのメタ計算
             context.stepOfAddTen++;
             goto addTen_stub(context);
         case Twice:
@@ -293,6 +267,7 @@
 メタ計算の例として、メモリ管理の他にも例外処理や並列実行、ネットワークアクセスなどがある。
 通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。
 
+
 \section{CbC で記述した非破壊赤黒木}
 CbC で記述されたデータ構造に赤黒木がある。
 赤黒木とは木構造のデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
@@ -325,8 +300,6 @@
 赤黒木で利用する Data Segment を表\ref{src:stack}に表す。
 Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。
 
-% TODO: Appendix でrbtreeのコード
-
 % {{{ 赤黒木の Data Segment
 
 \begin{table}[ht]
@@ -416,8 +389,6 @@
 akasha では仕様を Meta Code Segment に記述するため、CbCで常に真となる式として定義する
 赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(表\ref{src:specification})。
 
-%TODO akasha info はめた
-
 % {{{ 木の高さの仕様記述
 
 \begin{table}[ht]
@@ -609,28 +580,27 @@
 
 よって、CBMCでは検証できない範囲の検証をakashaで行なえることが確認できた。
 
-\section{まとめと今後の課題}
+\section{考察と今後の課題}
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
-CbC はCode SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。
-
-% 考察
+Code SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。
 
-% やってる範囲は今は小さい
-% どうすれば拡張できるか
+今回の検証では赤黒木が任意の順で有限の回数挿入されても木がバランスしていることを確認した。
+挿入順は深さ優先探索で総あたりで探索しているため、赤黒木の操作に削除が含まれると上手く数え上げられない。
+これは過去に探索した木の形状を記憶することで解決できる。
+また、挿入を行なった後の木の高さを調べるために毎回木をなぞるため、木の要素数に比例した計算時間がかかっている。
+各ノードに高さ情報を持たせ、木の操作時にノードの高さも更新することで高速に仕様をチェックすることができる。
+ノードの高さ情報そのものの処理が正しいかといった、メタ計算の仕様も検証したい。
+Meta Code Segment は任意の Code Segment に適用できるため、 akasha そのものの性質も akasha で検証できると考えている。
+加えて、今回の検証に用いたメタ計算は赤黒木へのデータ構造に依存している部分が多い。
+ポインタへの不正アクセス検出といった汎用的な検証機能をCBMCのように akasha にも追加していきたい。
 
-今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
-CBMCではポインタへの不正アクセスを行なう実行例を検出する機能が組込みで存在している。
-akashaでも一般的なエラーに対するメタ計算などを定義したい。
-本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
-木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
-また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
-さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。
 
 \begin{thebibliography}{9}
 
+\bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
+\bibitem{cite:rbtree} 小久保 翔平, 河野真治: Code Segment と Data Segment を持つ Gears OS の 設計 (2016)
 \bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
-\bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
-\bibitem{cite:rbtree} 小久保 翔平, 河野真治: Code Segment と Data Segment を持つ Gears OS の 設計 (2016)
+\bibitem{cite:dpp}  下地 篤樹, 河野 真治: 線形時相論理によるContinuation based Cプログラムの検証, 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), (2007)
 \bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991).
 \bibitem{cite:cbmc} Clarke, Edmund and Kroening, Daniel and Lerda, Flavio: A Tool for Checking {ANSI-C} Programs, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)
 \bibitem{cite:agda} \verb/The Agda Wiki - Agda/ \urlj{http://wiki.portal.chalmers.se/agda/pmwiki.php} \refdatej{2016-07-05}.
@@ -640,9 +610,11 @@
 
 \end{thebibliography}
 
+\appendix % TODO: red-black tree のコード
+
 \begin{biography}
 \profile{n}{比嘉健太}{1992年生。2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
-\profile{n}{河野真治}{1959年生。1984年3月東京工業大学理学部化学科卒業。1986年3月東京大学大学院情報工学課程修了。1989年5月工学博士。 1989-1996年 Sony Computer Science Laboratry, Inc. 1996年 琉球大学准教授。
+\profile{n}{河野真治}{1959年生。1984年3月東京工業大学理学部化学科卒業。1986年3月東京大学大学院情報工学課程修了。1989年5月工学博士。 1989-1996年 Sony Computer Science Laboratory, Inc. 1996年 琉球大学准教授。
 情報処理学会, ACM , 日本ソフトウェア科学会各会員。
 }
 \end{biography}