--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/midterm.tex	Tue Oct 15 17:24:29 2019 +0900
@@ -0,0 +1,91 @@
+\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}
\ No newline at end of file