\documentclass[submit,PRO]{ipsj}
\usepackage{PROpresentation}
\PROheadtitle{y-n-(x): 情報処理学会プログラミング研究会 発表資料 Y年m月d日}

\usepackage[dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}
\lstset{
  language={C},
  basicstyle={\small},
  commentstyle={\small\itshape},
  keywordstyle={\small\bfseries},
  stringstyle={\small},
  frame={trlb},
  breaklines=true,
  columns=[l]{fullflexible},
  xrightmargin=0zw,
  xleftmargin=3zw,
  lineskip=-0.5ex,
  captionpos=b,
  moredelim=**[s][\color{red}]{\"compressed}{\"},
}
\renewcommand{\lstlistingname}{Code}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}

\setcounter{巻数}{57}
\setcounter{号数}{1}
\setcounter{page}{1}

% TODO: コードセグメント, Code Segment の統一


\受付{2015}{3}{4}
%\再受付{2015}{7}{16}   %省略可能
%\再再受付{2015}{7}{20} %省略可能
\採録{2015}{8}{1}




\begin{document}


\title{Continuation based C を用いたプログラムの検証手法}
\etitle{Verification method of programs using Continuation based C}

\affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\
Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus}
\affiliate{RUniv}{琉球大学\\
University of the Ryukyus}


\author{比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
% TODO: update
Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。
\end{abstract}


\begin{jkeyword}
プログラミング言語, 検証, 赤黒木
\end{jkeyword}

\begin{eabstract}
% TODO: update
We propose a verification method for programs using Continuation based C language.
Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
Code segments are calculation units which have input/output data segments that data unit.
Programs are represented by connections among with code segments and code segments.
The output data segment of some code segment is converted to the input data segment of connected one.
We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more.
Meta computations represented to meta code segment and meta data segment, which saves main computations.
In this paper, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree and Synchronized Queue.
\end{eabstract}

\begin{ekeyword}
Programming Language, Verification, Red-Black Tree
\end{ekeyword}

\maketitle

\section{コードセグメントとデータセグメント}
本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法やプログラムの状態を全て数えあげるモデルチェッカなどが存在する。 % TODO ref
しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。

実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref?
コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。
プログラムはコードセグメントどうしを組み合わせることにより構築される(図\ref{fig:csds})。
組み合わせる際のコードセグメント間における値の受け渡しにはデータセグメントを用いる。
データセグメントとはデータの単位である。
なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。

\begin{figure}
    \begin{center}
        \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf}
        \caption{コードセグメントどうしの組み合わせ}
        \label{fig:csds}
    \end{center}
\end{figure}

ここで、コードセグメントどうしの接続処理について考える。
処理を表すコードセグメントどうしの接続も処理であるため、コードセグメントで表現できる。
このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
また、メタ計算に必要なデータはメタデータセグメントに格納する。
メタデータセグメントは通常の処理に必要なデータセグメントの拡張である。
プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。

\section{Continuation based C}
コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。
Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。

\begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)]
__code addTen(int a) {
    int b = a+10;
    goto twice(b);
}

__code twice(int x) {
    int y = 2*x;
    goto showValue(y);
}
\end{lstlisting}

CbCにおけるコードセグメントは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
コードセグメント内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
次のコードセグメントへ接続する場合は \verb/goto/ を用いて接続先を指定する。
Code\ref{src:simpleCs}の例では、2つのコードセグメント \verb/addTen/ と \verb/twice/を定義している。
\verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
\verb/twice/では受けとったintの値を2倍して \verb/showValue/ を実行する。

また、CbCにおけるデータセグメントはC言語における構造体と共用体を用いたデータ構造である。
各コードセグメントで必要な値を構造体で定義し、それらの共用体としてデータセグメントを定義する(Code\ref{src:simpleDs})。

\begin{lstlisting}[label=src:simpleDs, caption=data]%データセグメントの例 (10加算して2倍する)]

union Data {
    struct Count {
        int x;
    } count;
    struct Port {
        unsigned int port;
    } port;
};
\end{lstlisting}

Code\ref{src:simpleDs}ではデータセグメントとして int を持つ count と unsigned int を持つ port の2つを定義している。
コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる。

\begin{lstlisting}[label=src:stub, caption=stub]%データセグメントの利用例 (countの値を2倍する)]

__code addTen(union Data* ds, int a) {
    int b = a+10;
    goto twice_stub(ds);
}

__code twice_stub(union Data* ds) {
    goto twice(ds->count.x);
}

__code twice(int x) {
    int y = 2*x;
    goto showValue(y);
}
\end{lstlisting}

Code\ref{src:stub}では \verb/twice/ の際に2倍する値は count の値であることを \verb/twice_stub/ で指定している。
CbC におけるメタコードセグメントはCode\ref{src:stub}や goto する際に必ず通るコードセグメント(Code\ref{src:meta}の \verb/meta/)のように表現される。

\begin{lstlisting}[label=src:meta, caption=meta ] %メタコードセグメントを用いて接続した例]

struct Context {
    union Data *data;
    /* メタ計算に必要なデータ */
};

__code meta(struct Context* context,
            enum Code next) {

    /* 接続時に行なうメタ計算を記述 */
    switch (next) {
        case AddTen:
            /* 特定のコードセグメントへのメタ計算 */
            goto addTen_stub(context);
        case Twice:
            goto twice_stub(context);
    }
}

__code addTen(struct Context* context, int a) {
    x = x+10;
    goto meta(context, Twice);
}

__code twice(struct Context* context, int x) {
    x = x*2;
    goto meta(context, ShowValue);
}
\end{lstlisting}

メタコードセグメントの切り替えは \verb/meta/ を変更することで実現できる。
また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現できる。

CbC におけるメタ計算の例にメモリ管理がある。
メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。

\section{メタ計算を用いたデータ構造の性質の検証}
CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。
検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{gears-os}における非破壊赤黒木を用いる。
赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。

まず、検証を行なうために満たすべき仕様を定義する。
仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する(Code\ref{src:specification})。

\begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述]

if (akashaInfo.maxHeight >
    2*akashaInfo.minHeight) {
   goto meta(context, ShowTrace);
}

\end{lstlisting}

定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。

当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。
akasha では検証用の仕様をメタコードセグメントに定義する。
検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。
akasha を用いて要素数13個までは任意の順で挿入を行なっても仕様が満たされることを検証した。
また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。

CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。
任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。
しかし、cbmcで検証できる範囲内では赤黒木の仕様を検証することはできなかった。
有限モデルチェッカでは探索する状態空間を有限の数で指定し、それを越える範囲は探索しない。
cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。

\section{まとめと今後の課題}
コードセグメントとデータセグメントを用いたプログラミング手法を用いる言語CbCで記述したプログラムに対する仕様の検証を行なうことができた。
メタ計算として検証を行なうことで、実際に動作するプログラムを全く変更することなくプログラムを検証した。

今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。

\begin{thebibliography}{9}

\bibitem{cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
\bibitem{gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)

\end{thebibliography}

\begin{biography}
\profile{n}{比嘉健太}{2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
% TODO: update
\profile{n}{河野真治}{1960年生．1982年情報処理大学理学部情報科学科卒業．
1984年同大学大学院修士課程修了．1987年同博士課程修了．理学博士．1987年情報処
理大学助手．1992年架空大学助教授．1997年同大教授．オンライン出版の研究
に従事．2010年情報処理記念賞受賞．電子情報通信学会，IEEE，IEEE-CS，ACM
各会員．}
\end{biography}



\end{document}