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

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



\usepackage[dvips]{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{xv6の構成要素の継続の分析}

%\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}

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


\author{清水 隆博}{Shimizu Takahiro}{KIE}[anatofuz@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。

状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
\end{abstract}


\maketitle

\section{OSの信頼性}
様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
テスト以外の方法でOSの信頼性を高めたい。

数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
これに適した形として、 状態遷移モデルが挙げられる。
OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。
分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語を用いて再実装することで仕様の整合性を検証する事が可能である。
しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。
実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。

実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。

現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。

\section{xv6 kernel}

xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。

xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。

本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイルディスクリプタがある。


\section{Continuation Based C}

Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックにjmp命令で移動する継続が導入されている。
この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
またCbCではこの軽量継続を用いた再帰呼び出しを利用することで、 for文などのループ文を廃し関数型プログラミングに近いスタイルでプログラミングすることが可能である。
現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。

\nocite{*}
\bibliographystyle{ipsjunsrt}
\bibliography{anatofuz-bib}


\end{document}