\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 では拡張性と信頼性を両立させることが要求されている。
信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。

Gears OS は Continuation based C (CbC) によってアプリケーションと OS そのものを記述する。
OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、
エラーハンドリング等の記述しなければならない処理が存在する。
これらの計算をメタ計算と呼ぶ。
メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。
CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。

OS は時代とともに複雑さが増し、OS の信頼性を保証することは難しい。
そこで、基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、OS の機能を保証する。

Code Gear は goto による継続で処理を表すことができる。
これにより、状態遷移による OS の記述が可能となり、複雑な OS のモデル検査を可能とする。
また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。
これらを用いて OS の信頼性を保証したい。

CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要があり、
機能を接続するAPIと実装の分離が可能であることが望ましい。
Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。

本論文では、Interface を用いたモジュールシステムの説明と、
xv6 の CbC 書き換えについての考察を行う。


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

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

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




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

\subsection{今後}
\subsection{}

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

\end{thebibliography}
\end{document}