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

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



\usepackage[dvips,dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}
\lstset{
  language=C,
  tabsize=2,
  frame=single,
  basicstyle={\tt\footnotesize}, %
  identifierstyle={\footnotesize}, %
  commentstyle={\footnotesize\itshape}, %
  keywordstyle={\footnotesize\ttfamily}, %
  ndkeywordstyle={\footnotesize\ttfamily}, %
  stringstyle={\footnotesize\ttfamily},
  breaklines=true,
  captionpos=b,
  columns=[l]{fullflexible}, %
  xrightmargin=0zw, %
  xleftmargin=1zw, %
  aboveskip=1zw,
  numberstyle={\scriptsize}, %
  stepnumber=1,
  numbersep=0.5zw, %
  lineskip=-0.5ex,
}
\usepackage{caption}


\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}
\renewcommand{\lstlistingname}{Code}

\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言語などでの実装の段階で発生するバグを取り除くことができない。
実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。

さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。
本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。
ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。
プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。

ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。

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



\section{Continuation Based C}

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


CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。
入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。
これらの関係図を図\ref{fig:cgdg}に示す。

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{fig/cgdg.pdf}
    \end{center}
    \caption{CodeGearと入出力の関係図}
    \label{fig:cgdg}
\end{figure}

CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
例題ではCodeGearとして\texttt{factorial}を宣言している。
\texttt{factorial}はCodeGearの引数として\texttt{struct F}型の変数\texttt{arg}を受け取り、\texttt{arg}のメンバー変数によって\texttt{factorial}の再帰呼び出しを行う。
CodeGearの呼び出しは\texttt{goto}文によって行われる。
この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。
図中の四角がDataGear、 円がCodeGearに対応する。


\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める例題}]
__code factorial(struct F arg) {
    if (arg.n<0) {
        exit(1);
    }
    if (arg.n==0) {
      goto arg.next(arg);
    } else {
      arg.r *= arg.n;
      arg.n--;
      goto factorial(arg);
    }
}
\end{lstlisting}

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{fig/factorial_cbc.pdf}
    \end{center}
    \caption{CbCで階乗を求める例題の状態遷移}
    \label{fig:factorial_cbc}
\end{figure}

CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。

この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
これはGCCでは内部コードを生成、 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。

\section{CbCを用いたOSの実装}

軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。
現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。

GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、　現在はPerlスクリプトによってGearsOSのビルド時に生成される。
CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{./fig/meta-cg-dg.pdf}
    \end{center}
    \caption{CodeGearとMetaCodeGear}
    \label{meta-cg-dg}
\end{figure}

通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。
この流れを図\ref{meta-cg-dg}の上段に示す。
しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearを保存場所から取り出すMetaDataGearなどのメタ計算が加わる。
これは図\ref{meta-cg-dg}の下段に対応する。

遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとしてcontextがある。
contextは処理に必要なCodeGearの番号とMetaCodeGearの対応表や、 DataGearの格納場所を持つ。
計算に必要なデータ構造と処理を持つデータ構造であることから、 contextは従来のOSのプロセスに相当するものと言える。
cotnextと各データ構造の関わりを図\ref{fig:context_ref}に示す。
\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{fig/Context_ref.pdf}
    \end{center}
    \caption{Contextと各データの関係図}
    \label{fig:context_ref}
\end{figure}

コード上では別のCodeGearに直接遷移している様に見えるが、 実際はcontext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。
MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、　実際の計算が行われる。


\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のファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。

本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、　仮想メモリなどのOSの根幹部分でそれぞれ行った。


\section{xv6のシステムコールの継続の分析}
xv6の処理を継続を中心とした記述で再実装を行う。
この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。

まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。
分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=80mm]{fig/readsyscall_state.pdf}
    \end{center}
    \caption{readシステムコールの状態遷移}
    \label{fig:cbc_readsyscall}
\end{figure}

CbCで再実装した\texttt{read}システムコールは、 xv6の\texttt{read}システムコールのディスパッチ部分から、 \texttt{cbc\_read}CodeGearに\texttt{goto}文で軽量継続される。
継続後はreadする対象によって\texttt{cbc\_readi}や、 \texttt{cbc\_consoleread}などに状態が変化していく。
各CodeGearの遷移時にはDataGearがやり取りされる。
DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。

この実装の利点として、 CodeGearの命名と状態が対応しており、 状態遷移図などに落としても自然言語で説明が可能となる点が挙げられる。
しかし実際には\texttt{cbc\_readi}の状態はさらに複数のCodeGearに分離しており、 実際に\texttt{read}システムコールを実装するCodeGearの数は図の状態より多い。
この事から、 複数のCodeGearを1つにまとめた上で見た状態と、 各CodeGearそれぞれの状態の2種類の状態があるといえる。

複数のCodeGearをまとめた状態は、 抽象化したAPIの操作時におけるアルゴリズム上の問題が無いかの確認として使用出来る。
対して各CodeGearそれぞれはモデル検査や、 特定の関数の中の処理が適しているかどうかの検査として見ることが出来ると考えられる。

この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。
Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。
xv6の処理をCbCで再実装する際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。

\section{xv6のシステムコール以外の継続の分析}
xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。
これらはOSの立ち上げ時やシステムコールの中で、ファイルシステムの操作に対応した関数や構造体などのAPIを通して操作される。

\section{Basic Blockに基づく分析}

xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。
この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。

まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。
CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することで状態遷移系への変換を行った。



\section{CbCを用いた部分的なxv6の書き換え}

CbCではCodeGear、 DataGearからなる単位を基本とし、 それぞれにメタなGearが付随する。
また実行に必要なCodeGearとDataGearをまとめたcontextというMetaDataGearが存在する。
この機能を元にxv6の書き換えを検討した。

xv6内でCbCの軽量継続に突入する際は、 元の処理関数に通常の方法では戻ってくることができず、部分的に書き換えていくのが困難である。
今回は呼び出し関数に戻れるスタックフレームを操作したい為に、 ダミーの\texttt{void}関数を用意した。
この関数内でCodeGearに\texttt{goto}文を用いて遷移することで、 CbCから帯域脱出した際に\texttt{void}関数の呼び出し元から処理を継続し、部分的にCbCに書き換えることが可能となった。
Code\ref{src:dumy_function_cbc}では、 \texttt{userinit}関数へ戻るために、 \texttt{cbc\_init\_vmm\_dumy}を経由している。

\begin{lstlisting}[frame=lrbt,label=src:dumy_function_cbc,caption={部分的にCbCを適応する例}]
void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz)
{
    struct vm* vm = createvm_impl(cbc_context);
    goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
}

void userinit(void)
{
// omission

    if((p->pgdir = kpt_alloc()) == NULL) {
        panic("userinit: out of memory?");
    }

    cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);

    p->sz = PTE_SZ;
    memset(p->tf, 0, sizeof(*p->tf));
\end{lstlisting}


\section{xv6の今後の再実装}

xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
グローバル変数を極力使わず継続を中心とした実装を行いたい。

contextは現在プロセス構造体に埋め込まれており、　kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。

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


\end{document}