# HG changeset patch # User e165723 # Date 1571558819 -32400 # Node ID afaa3a0ba58dab6d6af9be19aa2c1936615a3ba5 # Parent f0db7d006b4f2a28287cceb6f36490ed905eb1d6 fix diff -r f0db7d006b4f -r afaa3a0ba58d midterm.mm --- a/midterm.mm Sat Oct 19 14:48:19 2019 +0900 +++ b/midterm.mm Sun Oct 20 17:06:59 2019 +0900 @@ -2,22 +2,22 @@ - - + + - - + + + + + - - - - + - - - + + + diff -r f0db7d006b4f -r afaa3a0ba58d midterm.tex --- a/midterm.tex Sat Oct 19 14:48:19 2019 +0900 +++ b/midterm.tex Sun Oct 20 17:06:59 2019 +0900 @@ -62,16 +62,28 @@ \section{研究目的} +呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる. +つまり.CbCのinterfaceを使うとモジュール化とOS内部の明確化がstackなしで実現できる. + +本研究ではこれらのことを用い,xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし,OSの信頼性を保証したい. + \section{Continuation based C} -xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語Continuation based C (CbC)を用いる. -CbCは基本的な処理単位をCodeGearとして定義し,CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. +xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる. +CbC は基本的な処理単位を CodeGearとして定義し,CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. +CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する. +またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ. -%\lstinputlisting[label=cbcexample, caption=cbc\_example.cbc]{src/cbc_example.cbc} +%CbCは軽量継続を中心にプログラミングする事が可能であるため,レジスタの移動などが行われない. +%その為並列化やループ制御,関数呼び出しにおけるスタック制御などを意識したプログラミングスタイルでプログラミングする事が可能である. -\section{xv6} -xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. -\\xv6はシンプルでUnixに似た構造を持っている. - +\section{CbCのAgdaForm} +CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー>ってことを書けば良い? +\section{CbCのcontext} +CbCのcontextには引数の置き場所が書いてある.引数の置き場所とはCodeGearのことでありCodeGearには引数が格納されている?. +番号で管理している。 +dataの保存先と実行するdategearの保存先 +パルスさんの修論 +コンテキストには引数置き場所が書いてあるー>CodeGear \section{xv6のinterface} \section{今後の課題}