\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 の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。現段階で動作する OS として xv6 を採用し、 CbCで書き換えることにより stackを排除し状態遷移化することができる。状態遷移化することにより状態を有限化させることが可能となるため、評価が容易になる。よって評価を容易にするためにxv6 kernel をCbC で書き換え状態遷移に落とし込むことを目的とする。


\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 を全て持っている Meta Data Gear で ある。Context は通常の OS のスレッドに対応する。

\subsection{Interface}

\section{xv6 のCbCへの書き換え}

\subsection{書き換え}

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

\subsection{今後}
\subsection{}

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

\end{thebibliography}
\end{document}