%%
%% 研究報告用スイッチ
%% [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{Gears OSとCbC}

Gears OS は軽量継続を基本とする言語CbCを用いたOSの実装である。アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。
信頼性を保証する一つの方法は、プログラムの可能な実行を数え上げて要求仕様を満たしているかどうかを調べるモデル検査である。
本論文では、Gears OS上のアプリケーション、さらに Gears OSそのものをGears OS上でモデル検査することに関して考察する。

CbC (Continuation based C)はCの機能を持ち、goto 文で遷移する codeGearという単位を持っている。通常の関数呼び出しと異なり、stackや環境を
隠して持つことがなく、計算の状態は codeGear の入力ですべて決まる。codeGearの入力は dataGearと呼ばれる構造体だが、これには
ノーマルレベルのdataGearとメタレベルのdataGearの階層がある。メタレベルには計算を実行するCPUやメモリ、計算に関与するすべてのノーマルレベルの
dataGearを格納する context などがある。context は通常のOSのプロセスに相当する。

メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを
呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。

    ノーマルレベルのcodeGaerのgoto

    メタレベルのでのcodeGaerのstub と goto meta

ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された
通りに実行される必要がある。これは一般的には保証されない。他のcodeGearが共有された dataGearに競合的に書き込んだり、割り込みにより処理が
中断したりする。しかし、Gears OS が codeGear が正しく実行さることを保証する。つまり、Gears OS はそのように実装されているとする。

プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。後者は並列実行される codeGear の順列並び替えになる。従って、
これらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれればモデル検査を実装できることになる。

ただし、context の状態は有限状態になるとは限らないし、有限になるとしても巨大になることがある。しかし、OSやアプリケーションのテストだと
考えると、それらの動作の振る舞いを調べるのに十分な状態があれば良い。一つの方法は context の状態をなんらかの方法で抽象化することである。

本論文では context の中の状態を特定するのに必要なメモリ領域を登録する手法を用いる。メモリ領域はcontextの中のアドレスとサイズで指定される。
その中に格納されるのはノーマルレベルのdataGearとメタレベルのdataGearになる。ノーマルレベル側にはアドレスは格納されないと仮定する。
これは、ノーマルレベルの計算は末尾再帰な関数型プログラミングと仮定するのとだいたい同等である。現在は Agda (Haskell上の定理証明系の関数型言語)\cite{}
で記述することを考えている。 メタレベル側にはメモリアドレスなどが直接入ることになる。

メモリ領域の集合で一つの状態が定義される。この状態をさらに格納するデータベースを用意する。codeGearのシャッフルの深さ優先探索を行ない、新しく生成された
状態をデータベースで参照し、既にあれば、深さを一つ戻り、別な探索枝に移る。新しい状態が生成されてない、あるいは、バグを見つければモデル検査は
終了と言うことになる。

ここでは例題として Dining Phisopher 問題のdead lockの検出を行う。
研究の段階としては

(1)  Dining Phisopherを Gears OS上のアプリケーションとして実装する(DPP)。
(2) DPPをcodeGearのシャッフルの一つして実行する meta codeGear を作成する。
(3) 可能な実行を生成する iterator を作成する。
(4) 状態を記録する memory 木と状態DBを作成する。

この段階でDPPのモデル検査が可能になるはずである。

一方で Gears OSそのものも codeGear で記述されている。CPU毎のC.context、そして、それが共有するKernelのK.context、それからユーザプログラムのU.context
などの context からなる。これら全体は meta dataGear である K.context に含まれている。

U.context がDPPのように単純なものならばOS全体のcontextも複雑にはならない。したがって、これ全体を Gears OSで実行することが可能である。

(5) Gears OSを含む codeGear のシャッフル実行を行ない、モデル検査を実現する

これにより、Gears OSの自分自身によるモデル検査が可能になる。この時に、検査するcodeGearと検査されるcodeGearは同じ物であるが、
実行する meta codeGarが異なっている。現状では、これは異なるmeta codeGearを指定してコンパイルしなおすことにより実現する。

Gears OSの実装は Unix 上のアプリケーションとしての実装と、x.v6\cite{}の書き換えによる実装の二種類があるが、前者ではアプリケーションは
OSに直接リンクされる。後者では x.v6 のexec機構により実行される。実際にOSのモデル検査を実行するためには、必要なmeta dataGear/meta codeGear
の emulatorを書く必要がある。しかし、検査する必要がない部分は無視できるようにしたい。

Gears OSは並列実行機構を持っているので、

(6) モデル検査を並行実行することができる

はずである。


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