\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}

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

% TODO lstlisting のcaptionの修正


\begin{document}

% ipsjpro
%     llrb の実装を書いても良い
%         stack の話とか
%     どうやって akasha で検証しているか
%     cbmc でできなかった理由とかも書く
%         実際はフェアじゃないし
%
% --- たけだくんから ---
% Attonさん
%
% オブジェクトレベルがないとのだれも論文はわからない
% meta levelの話がいきなり来ている
% stub
%
% どれがメタでどれがオブジェクトがちゃんと書いたほうがいい
%
% メタとstubの関係
% 今のred black treeがあんまり綺麗に書かれてないのがそもそも問題
% sm
% new smvとかちゃんと知ってますよと書いたほうがいいかも・・・
%
% 同じようなことをやってる人の論文を見るといいかも
% 背景などもわかるかも
%
% Treeの大きさがどれくらいなのかという図
% CBCで書かれたRed black Treeも書いた方がいい
%
% 検証できる範囲を検証できなかったというのはおかしい
%
% うりとしては実コードで検証できる
% 挿入する要素数がある程度あれば
%
% Treeeをランダムに生成する
%
% なぜswitchを入れている？
% セグフォした時に前のコードがわからない
% ー＞デバッグ用のコード
%
% 次のためにみたいなので
% const struct Node* node = akashaInfo -> akashaNode-> Node;の go toの部分
%
% red black treeで2ページぐらいでスタックの部分ももりもり書いてもいい
%
% なぜcbcで苦労して書くのか？
% toy program的なのを書きたい
%
% パルスさんの書いたコンピテーション部分を持ってく
% kkbさんの修論があればいいなぁ
%
% ポインターの計算とかはAkashaにはない
% cbmcであればこういう風に書けば検証できる

\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}
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 によって記述された赤黒木といったデータ構造の性質を検証する。
\end{abstract}


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

\begin{eabstract}
We propose a verification method for executable 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.
\end{eabstract}

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

\maketitle

\section{ソフトウェアの検証}
ソフトウェアの規模が大きくなるにつれ、バグは発生しやすくなる。
バグとはソフトウェアが期待される動作とは異なる動作を行なうことである。
また、ソフトウェアの期待される動作を定義したものは仕様と呼ばれ、自然言語や論理で記述される。
検証とは、ソフトウェアが定められた環境下において仕様を満たすことを保証するものである。
ソフトウェアが仕様を満たすことを保証する手法として、定理証明とモデル検査がある。
定理証明はプログラムが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
定理証明を行なう言語には Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
モデル検査を行なうモデル検査器には、 promela と呼ばれる言語でモデルを記述する spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、C言語を記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
証明やモデル検査器で検証を行なう際、実際に動作するコードでなく証明用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
本研究は実際に動作するプログラムの信頼性を保証することを目的とする。

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

\begin{figure}
    \begin{center}
        \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf}
        \caption{Code Segmentどうしの組み合わせ}
        \label{fig:csds}
    \end{center}
\end{figure}

ここで、Code Segmentどうしの接続処理について考える。
処理を表すCode Segmentどうしの接続も処理であるため、Code Segmentで表現できる。
このような、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。
Meta Code SegmentはCode Segment間に存在する上位の処理と考えることもできる(図\ref{fig:metaCSDS})。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.5]{fig/meta_code_segment_and_meta_data_segment.pdf}
        \caption{Meta Code Segment と Meta Data Segment}
        \label{fig:metaCSDS}
    \end{center}
\end{figure}

また、メタ計算に必要なデータはMeta Data Segmentに格納し、通常の処理に必要なData Segmentも内包する。
プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。

\section{Continuation based C}
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})。
軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。

% {{{ Code Segment の接続(10加算して2倍する)
\begin{table}
\begin{lstlisting}
__code addTen(int a) {
    int b = a+10;
    goto twice(b);
}

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

\end{lstlisting}
\caption{Code Segment の接続(10加算して2倍する)}
\label{src:simpleCs}
\end{table}
% }}}

CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
表\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。
\verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
\verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。

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

% {{{ Data Segment の例
\begin{table}[ht]
\begin{lstlisting}
union Data {
    struct Count {
        int x;
    } count;
    struct Port {
        unsigned int port;
    } port;
};
\end{lstlisting}
\caption{Data Segmentの例}
\label{src:simpleDs}
\end{table}
% }}}

表\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
Code Segment 内部では演算やポインタ演算は行なわず、メタ計算部分でポインタへの演算を行なう。
これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。
Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(表\ref{src:stub} における \verb/twice_stub/)。
CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。

% {{{ Data Segment を指定する Meta Code Segment
\begin{table}[ht]
\begin{lstlisting}
// Code Segment
__code addTen(union Data* ds, int a) {
    int b = a+10;
    goto twice_stub(ds);
}

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

// Code Segment
__code twice(int x) {
    int y = 2*x;
    goto showValue(y);
}
\end{lstlisting}
\caption{Data Segment を指定する Meta Code Segment}
\label{src:stub}
\end{table}

% }}}

CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(表\ref{src:meta} における Context)。
また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(表\ref{src:meta} における \verb/meta/)。
\verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。

% {{{ Code Segment を接続するメタ計算メタ計算として接続した例

\begin{table}[ht]
\begin{lstlisting}

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

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

    /* 接続時に行なうメタ計算を記述 */
    switch (next) {
        case AddTen:
            /* 特定のCode Segmentへのメタ計算 */
            goto addTen_stub(context);
        case Twice:
            goto twice_stub(context);
    }
}

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

// Code Segment
__code twice(struct Context* context, int x) {
    x = x*2;
    goto meta(context, ShowValue);
}
\end{lstlisting}
\caption{Code Segment を接続するメタ計算メタ計算として接続した例}
\label{src:meta}
\end{table}

% }}}

メタ計算の例として、メモリ管理の他にも例外処理や並列実行やネットワークアクセスなどがある。
通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。

\section{CbC で記述した赤黒木}
CbC で記述されたデータ構造に赤黒木がある。
赤黒木とは木構造のデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
赤黒木は通常の二分探索木としての条件の他に以下の条件を持つ。

\begin{itemize}
    \item 各ノードは赤または黒の色を持つ。
    \item ルートの色は黒である。
    \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)。
    \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
\end{itemize}

これらの条件により、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる。

赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木がある。
非破壊赤黒木とは木への挿入や削除を行なった際に一度構築した木構造を破壊することなく新しく木構造を生成する赤黒木である。
非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することで実現できる。

%TODO figure

関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC はgotoによる軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
辿った経路を記憶するため Meta Data Segment にスタックを持たせる。
このスタックは軽量継続ではなく関数呼び出しで利用する。

赤黒木の赤が続かないという制約をチェックする Code Segment は表\ref{src:rbtree}のようになる。
まず、親の情報が必須なために経路を記憶しているスタックから親の情報を取得する。
親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
親の色が赤である場合は経路情報を再現するためにスタックへと親を挿入し、次の条件判定へと \verb/goto/ する。

% {{{ 赤黒木の赤が続かないという制約の判定

\begin{table}[ht]
\begin{lstlisting}

// Meta Code Segment
__code insertCase2(struct Context* context, struct Node* current) {
    struct Node* parent;
    stack_pop(context->node_stack, &parent);
    if (parent->color == Black) {
        stack_pop(context->code_stack, &context->next);
        goto meta(context, context->next);
    }
    stack_push(context->node_stack, &parent);
    goto meta(context, InsertCase3);
}

// Meta Meta Code Segment
__code insert2_stub(struct Context* context) {
    goto insertCase2(context, context->data[Traverse]->traverse.current);
}
\end{lstlisting}
\caption{赤黒木の赤が続かないという制約の判定}
\label{src:rbtree}
\end{table}

% }}}

ここで、赤黒木に対する処理を Code Segment とした場合、赤黒木のメモリ管理などは Meta Code Segment である。
赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。
このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能であり、検証機構の検証なども行なうことができる。


\section{メタ計算を用いたデータ構造の性質の検証}
CbC で記述された赤黒木と、それに対する処理の性質を実際に検証する。
また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。

まず、検証を行なうために満たすべき仕様を定義する。
仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
検証する仕様として、とを CbC で定義する(表\ref{src:specification})。

% {{{ 木の高さの仕様記述

\begin{table}[ht]
\begin{lstlisting}
if (akashaInfo.maxHeight >
    2*akashaInfo.minHeight) {
   goto meta(context, ShowTrace);
}
\end{lstlisting}
\caption{木の高さの仕様記述}
\label{src:specification}
\end{table}

% }}}

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

当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
-
akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
挿入順の数え上げには深さ優先探索を用いる。
CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。
各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。
要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。

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

よって、CBMCでは検証できない範囲の検証をakashaで行なうことが確認できた。

\section{まとめと今後の課題}
CbC で記述したプログラムに対する仕様の検証を行なうことができた。
CbC はCode SegmentとData Segmentを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。

今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
CBMCではポインタへの不正アクセスを行なう実行例を検出することができる。
akashaでも一般的なエラーに対するメタ計算などを定義したい。
本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。

\begin{thebibliography}{9}

\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: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}.
\bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991).

\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}