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

%\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}

\usepackage{comment}
\usepackage{listings}
\lstset{
  language=C, 
  tabsize=2, 
  frame=single, 
  basicstyle={\ttfamily\footnotesize}, % 
  identifierstyle={\footnotesize}, % 
  commentstyle={\footnotesize\itshape}, % 
  keywordstyle={\footnotesize\bfseries}, % 
  ndkeywordstyle={\footnotesize}, % 
  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, 
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small, tt}}

\renewcommand{\abstractname}{概要}
 
\begin{document}
\title{xv6 kernel上でのCbCによるinterfaceの実装\\CbC interface implementation in xv6 kernel}
\author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy} 

\section{研究目的}
当研究室ではOSの信頼性の保証と拡張性の実現のため, CbCを用いた Gears OSの研究を行なっている.
しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える.

%形式手法
CbC は 定理証明支援系 Agda に置き換えることができるように構築されている.
CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる.
本研究ではこれらのことを用い, xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし, OSの信頼性を保証したい.

%\section{GearsOS}

\section{xv6}
xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである.
xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI-Cに書き換えられ x86 に再実装された. xv6 はシンプルであるがUnixの概念と構造を持っている.
\section{Continuation based C}
xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる.
CbC は基本的な処理単位を CodeGearとして定義し，CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である.
CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する%図かコードを入れても良いかも
またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ.
現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている．



\section{CbCのAgdaForm}
%Agdaについて

%Agdaでなぜ説明できるか。飽和ロジック
%CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー＞ってことを書けば良い？


\section{context}

%CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し.
%番号で管理している。
%dataの保存先と実行するdategearの保存先

%パルスさんの修論

%コンテキストには引数置き場所が書いてあるー＞CodeGear
\section{xv6のinterface}
%呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる．
\section{今後の課題}

%\begin{thebibliography}{9}

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

%\end{thebibliography}
\end{document}