Binary file midterm.pdf has changed

--- a/midterm.tex	Sun Oct 20 17:06:59 2019 +0900
+++ b/midterm.tex	Sun Oct 20 18:29:56 2019 +0900
@@ -61,31 +61,45 @@
 \thispagestyle{fancy} 
 
 \section{研究目的}
+現代の OS では拡張性と信頼性を両立させることが要求されている．
+信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である．
 
-呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる．
-つまり.CbCのinterfaceを使うとモジュール化とOS内部の明確化がstackなしで実現できる.
+%形式手法
 
+つまり,CbCのinterfaceを使うとモジュール化とOS内部の明確化がstackなしで実現できる.
 本研究ではこれらのことを用い,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へ遷移する．
+CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する%図かコードを入れても良いかも
 またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ.
+現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている．
 
-%CbCは軽量継続を中心にプログラミングする事が可能であるため，レジスタの移動などが行われない．
-%その為並列化やループ制御，関数呼び出しにおけるスタック制御などを意識したプログラミングスタイルでプログラミングする事が可能である．
+
 
 \section{CbCのAgdaForm}
-CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー＞ってことを書けば良い？
-\section{CbCのcontext}
-CbCのcontextには引数の置き場所が書いてある.引数の置き場所とはCodeGearのことでありCodeGearには引数が格納されている?.
-番号で管理している。
-dataの保存先と実行するdategearの保存先
-パルスさんの修論
-コンテキストには引数置き場所が書いてあるー＞CodeGear
+%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}