\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvipdfmx]{graphicx} 
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage{listings}
\usepackage{caption}
\usepackage{latexsym}

%\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}

\begin{document}
\title{継続を用いたxv6 kernelの書き換え}
\author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy} 

\section{xv6を継続で書き換える意味}
現代の OS では拡張性と信頼性を両立させることが要求されている．
信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である．

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


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

これらを用いて OS の信頼性を保証したい．
CbCの有効性を示すために，基本的な機能を揃えた OS である xv6 を CbC で書き換える.
これにより，OS の個々のシステムコールの持つ状態を明確にすることができると考えている.

CbC でシステムやアプリケーションを記述するためには，Code Gear と Data Gear を柔軟に再利用する必要があり，
機能を接続するAPIと実装の分離が可能であることが望ましい．
CbC では形式化されたモジュールシステムが提供されている. 
xv6 の CbC 書き換えでは, このモジュールシステムを用いる.

書き換えはまだ部分的であるが, 既存の部分と両立するように設計されている. 従って, xv6 の基本的な
動作には変更はない. 実際に実行速度などはほとんど差がない. 逆に言えばオーバヘッドが存在しないことが確認できた.


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

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

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

\section{section3}

\section{今後の課題}

%\begin{thebibliography}{9}

\nocite{*}
%\bibliographystyle{ipsjunsrt}
\bibliography{reference}

%\end{thebibliography}
\end{document}