comparison midterm.tex @ 4:afaa3a0ba58d

fix
author e165723 <e165723@ie.u-ryukyu.ac.jp>
date Sun, 20 Oct 2019 17:06:59 +0900
parents f0db7d006b4f
children f2089431388b
comparison
equal deleted inserted replaced
3:f0db7d006b4f 4:afaa3a0ba58d
60 \maketitle 60 \maketitle
61 \thispagestyle{fancy} 61 \thispagestyle{fancy}
62 62
63 \section{研究目的} 63 \section{研究目的}
64 64
65 呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる.
66 つまり.CbCのinterfaceを使うとモジュール化とOS内部の明確化がstackなしで実現できる.
67
68 本研究ではこれらのことを用い,xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし,OSの信頼性を保証したい.
69
65 \section{Continuation based C} 70 \section{Continuation based C}
66 xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語Continuation based C (CbC)を用いる. 71 xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる.
67 CbCは基本的な処理単位をCodeGearとして定義し,CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. 72 CbC は基本的な処理単位を CodeGearとして定義し,CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である.
73 CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する.
74 またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ.
68 75
69 %\lstinputlisting[label=cbcexample, caption=cbc\_example.cbc]{src/cbc_example.cbc} 76 %CbCは軽量継続を中心にプログラミングする事が可能であるため,レジスタの移動などが行われない.
77 %その為並列化やループ制御,関数呼び出しにおけるスタック制御などを意識したプログラミングスタイルでプログラミングする事が可能である.
70 78
71 \section{xv6} 79 \section{CbCのAgdaForm}
72 xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. 80 CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー>ってことを書けば良い?
73 \\xv6はシンプルでUnixに似た構造を持っている. 81 \section{CbCのcontext}
74 82 CbCのcontextには引数の置き場所が書いてある.引数の置き場所とはCodeGearのことでありCodeGearには引数が格納されている?.
83 番号で管理している。
84 dataの保存先と実行するdategearの保存先
85 パルスさんの修論
86 コンテキストには引数置き場所が書いてあるー>CodeGear
75 \section{xv6のinterface} 87 \section{xv6のinterface}
76 88
77 \section{今後の課題} 89 \section{今後の課題}
78 90
79 %\begin{thebibliography}{9} 91 %\begin{thebibliography}{9}