%%
%% 研究報告用スイッチ
%% [techrep]
%%
%% 欧文表記無しのスイッチ(etitle,eabstractは任意)
%% [noauthor]
%%

%\documentclass[submit,techrep]{ipsj}
\documentclass[submit,techrep,noauthor]{ipsj}



\usepackage[dvips,dvipdfmx]{graphicx}
\usepackage{latexsym}

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

%\setcounter{巻数}{59}%vol59=2018
%\setcounter{号数}{10}
%\setcounter{page}{1}


\begin{document}


\title{Gears OSでモデル検査を実現する手法について}

\affiliate{1}{琉球大学大学院理工学研究科情報工学専攻}
\affiliate{2}{琉球大学工学部工学科知能情報コース}
\affiliate{3}{琉球大学工学部}


\author{東恩納　琢偉}{Takui Higashionna}{1}[ikkun@cr.ie.u-ryukyu.ac.jp]
\author{奥田　光希}{Okuda Kouki}{2}[Koki.okuda@cr.ie.u-ryukyu.ac.jp]
\author{河野　真治}{Shinji kono}{3}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
GeasOSはCbCで記述されており処理単位であるcodeGearの間に自由にメタ計算をはさむことができる。ここにdataGearの状態を記録することにより、ユーザプロセスあるいはカーネルそのもののモデル検査が可能になる。一般的なモデル検査では状態数の爆発は避けられない。記録する状態を抽象化あるいは限定する手法について考察する。
\end{abstract}


%
%\begin{jkeyword}
%情報処理学会論文誌ジャーナル，\LaTeX，スタイルファイル，べからず集
%\end{jkeyword}
%
%\begin{eabstract}
%This document is a guide to prepare a draft for submitting to IPSJ
%Journal, and the final camera-ready manuscript of a paper to appear in
%IPSJ Journal, using {\LaTeX} and special style files.  Since this
%document itself is produced with the style files, it will help you to
%refer its source file which is distributed with the style files.
%\end{eabstract}
%
%\begin{ekeyword}
%IPSJ Journal, \LaTeX, style files, ``Dos and Dont's'' list
%\end{ekeyword}

\maketitle

%1
\section{並列プログラムの信頼性}
　現在、CPUの処理性能はクロック数の向上は電力消費の増大の問題から伸び悩んでおり、マルチコアCPUやGPUを利用した並列化処理を行うことによって処理速度の向上を図る事が多く、また画像処理や機械学習の分野では並列化処理は重要な役割を果たしている。しかし処理を並列化する場合、個々のプログラムが正しく動作する事が証明されていてもそれらを並列に実行したとき、全体の動作の正しさは保証されない。これは並列化されたプログラムの非決定性によるものである。また非決定性を含むプログラムは、逐次型のプログラムに有効な二分法などによるうデバック手法ではデバックする事が困難である。そのため、非決定生を含むプログラムに対して有効なデバック手法や検証手法の確立が重要な課題となっている。本研究ではモデル検査を用いる事でプログラムの信頼性を保証する手法として、GearsOSにおけるモデル検査手法について提案する。\\
　モデル検査とはプログラムのの設計から導出されたモデルが形式仕様を満たすかを検証することで信頼性を保証するもので、全ての状態を数えあげ、その状態について仕様が常に死んであることを確認する事で保証される。、しかしプログラムの規模が大きくなると導出されるモデルの状態数が爆発的に増えるためにそれら全てを検証する手法は好ましくない、そのため記録する状態を抽象化、または限定することによって検証の計算を減らす方法について考える。

\section{既存のモデル検査手法}
　モデル検査の方法としてよく利用される物として、SPIN と java path finder(以下JVM)というツールがある。\\
　SPIN は Promela という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。\\
SPIN では以下の性質を検査する事ができる。
\begin{itemize}
\item アサーション
\item デッドロック
\item 到達生
\item 進行性
\item 線形時相論理で記述された仕様
\end{itemize}
　Java Path Finder(JPF) は java プログラムに対するモデル検査ツールで、javaバーチャルマシン(JVM)を直接シミュレーションして実行している。そのため、javaのバイトコードを直接実行可能である。バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査する。バイトコードの実行パターンを網羅的に調べるために、膨大なCPU時間を必要とする。またJVMヘースであるため、複数のプロセスの取り扱いが出来ず、状態空間が巨大になる場合は直接実行は出来ず、一部を抜き出してデバックをするのに使用される。\\
JPF では以下の事ができる。
\begin{itemize}
\item スレッドの可能な実行全てを調べる
\item デッドロックの検出
\item アサーション
\item Partial Order Reduction
\end{itemize}

\newpage　
\section{Continuation based C}
　GearsOS は Continuation based C (以下CbC) という言語を用いて拡張性と信頼性を両立させることを目的として本研究室で開発されている。CbC はC言語と似た構文を持つ言語であるが、CodeSegment と DataSegment を用いるプログラミングスタイルを提案している。CodeSegmentは処理の単位である。CodeSegument は値を入力として受け取り処理を行ったあと出力を行う、また他の CodeSegment を接続していくことによりプログラムを構築していく。DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。DataSegmen は Input DataSegment と呼ばれ、出力はOutput DataSegment と呼ばれる。CodeSegment A と CodeSegment B を接続したとき、A の Output DataSegment は B の入力 Input DataSegment となる。
\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{./pic/input-outputDataSegment.pdf}
    \end{center}
    \caption{CodeSegment と DataSegment}
    \label{code-datasegment}
\end{figure}

CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずプログラムの検証を行なう。\\
　CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\ref{fig:meta_Gear}\\
  
\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=90mm]{./pic/meta_gear.pdf}
    \end{center}
    \caption{Gears OS のメタ計算}
    \label{meta_Gear}
\end{figure}

　GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、GPU環境では CodeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。\\


\section{DPP}
　検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\\
　5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。\\
　各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\
\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=70mm]{./pic/dpp_image.pdf}
    \end{center}
    \caption{Dining Philosohers Ploblem}
    \label{DPP_imag}
\end{figure}

 \section{タブロー展開と状態数の抽象化}
 　GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。タブロー法は生成可能な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\
　タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。

 \section{GearsOSを用いたモデル検査} 
　DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
　また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
　Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
　5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。
\begin{itemize}
\item Pickup Right fork
\item Pickup Left fork
\item eating
\item Put Right fork
\item Put Left fork
\item Thinking
\end{itemize}
この状態は goto next によって遷移する。またこの状態遷移は無限ループするのでMemoryTree に保管し、保管されている状態とはstat DB によって保管される
　

 

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=90mm]{./pic/model_checking.pdf}
    \end{center}
    \caption{DPP chacking}
    \label{DPP_chacking}
\end{figure}




\nocite{*}





\end{document}