\documentclass[submit,techrep,noauthor]{ipsj}
%\usepackage[dvips]{graphicx}
\usepackage{latexsym}
\usepackage[dvipdfmx]{graphicx} 
\usepackage{listings}
\usepackage{caption}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}
\def\lstlistingname{ソースコード}

\newcommand\coderef[1]{ソースコード \ref{code:#1}}

\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}


\begin{document}

\title{継続を用いたxv6 kernelの書き換え}

\paffiliate{IPSJ}{琉球大学工学部情報工学科\\
Information Engineering, University of the Ryukyus.}
\paffiliate{JU}{琉球大学大学院理工学研究科情報工学専攻\\
Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}

\author{坂本昂弘}{Takahiro SAKAMOTO}{IPSJ}
\author{桃 原 優}{Yu TTOBARU}{IPSJ}
\author{河野真治}{Shinji KONO}{IPSJ}

\begin{abstract}
xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている。当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で、用いることにより検証しやすくなる。xv6 を CbC で書き換えることで、 オペレーティングシステムの基本的な機能に対する検証を行うために書き換えを行う。
\end{abstract}




\maketitle

\section{はじめに}
OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。 xv6 はシンプルで扱いやすい基本的な構造を持つ OSである。このxv6 から Stack を排除することで OS の状態を有限化させることが可能となる。当研究室で開発している Continuation based C を用いてxv6 kernel を書き換えることでOSの状態を有限化可能であるかを検討する。

\section{Continuation based C}
\subsection{CbCの概要}
CbC は処理を Code Gear とした単位を用いて記述するプログラミング言語である。 Code Gear 間では軽量継続 (goto 文) による遷移を行うので、継続前の Code Gear に戻 ることはなく、状態遷移ベースのプログラミングに適している。図1 は Code Gear 間 の処理の流れを表している。

\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=70mm]{codesegment.pdf}
 \end{center}
 \caption{goto による code gear 間の継続}
 \label{fig:cbc}
\end{figure}

現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang、MicroCコンパイラ上で実装されている。今回 xv6 のkernelの部分をこの CbC を
用いて書き換える。

\subsection{Code Gear}
Code Gear は CbC における最も基本的な処理単位である。ソースコード \ref{codesegment} は CbC における Code Gear の一例である。
\begin{lstlisting}[frame=lrbt,label=codesegment,caption={code segmentの軽量継続}]
__code cs0(int a, int b){
  goto cs1(a+b);
}
__code cs1(int c){
  goto cs2(c);
}
\end{lstlisting}
Code Gear は\_\_code Code Gear 名 (引数) の形で記述される。Code Gear は戻り値を持 たないので、関数とは異なり return 文は存在しない。次の Code Gear への遷移は goto Code Gear 名 (引数) で次の Code Gear への遷移を記述する。ソースコード\ref{codesegment} での goto cs1(a+b); がこれにあたる。この goto の行き先を継続と呼び、このときの a+b が次の Code Gear への出力となる。Scheme の継続と異なり CbC には呼び出し元の環境がない ので、この継続は単なる行き先である。したがってこれを軽量継続と呼ぶこともある。cs1 へ継続した後は cs0 へ戻ることはない。軽量継続により、並列化、ループ制御、関数コー ルとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。
CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態 遷移ベースのプログラミングに適している。

\subsection{Data Gear}
Data Gear は CbC におけるデータの単位である。CbC では Code Gear は Input Data Gear、Output Data Gear を引数に持ち、任意の Input Data Gear を参照し、 Output Data Gear を書き出す。図 \ref{io}  Code Gear はこのとき渡された引数の Data Gear 以外を参照することはない。この Data Gear の対応から依存関係の解決を行う。

\begin{figure}[ht]
 \begin{center}
 \includegraphics[width=70mm]{IO_DataGear.pdf}
 \end{center}
 \caption{CodeGearとDataGear}
 \label{io}
\end{figure}

\section{Gears OSの概要}
Gears OS は Code Gear、Data Gear の単位を用いて開発されており、CbC で記述されている。Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っ ている Meta Data Gear を持つ。Gears OS は継続の際この Context を常に持ち歩き、必要な Code Gear、Data Gear を参照したい場合、この Context を通して参照する。

\subsection{Context}
Context は実行する Code Gear と Data Gear を全て持っており、通常 OS のプロセスに相当する。
また Context は Data Gear を構造体で定義しており、その全てを union と定義している。
Context 内で Code Gear と Data Gear は enumにより番号で管理されている。

\subsection{Interface}
Interface は Gears OS のモジュール化の仕組みである。Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。呼び出される Code Gear の引数となる Data Gear はここで全て定義される。Interface を定義 することで複数の実装を持つことができる。
CbC は関数呼び出しと異なり、goto による継続で遷移を行う。このため CbCの継続にはスタックフレームがなく引数を格納する場所がない。
Context は初期化の際に引数格納用の Data Gear の領域を確保する。Code Gear が継
続する際にはこの領域に引数の Data Gear を格納する。この領域に確保された Data Gear へのアクセスは Interface の情報から行われる。

\section{xv6 のCbCへの書き換え}
xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。xv6 はプロセス、仮想メモリ、カーネルとユーザ の分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、シンプルで学習しやすい。
CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。 xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。
\subsection{書き換え}

\section{結論}
\subsection{現状}

\subsection{今後}
\subsection{}

\begin{thebibliography}{9}
\bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、2019

\end{thebibliography}
\end{document}