# HG changeset patch # User e165723 # Date 1571642329 -32400 # Node ID 472b765acb14783621b19db7a2e35dd58aa7d4bc # Parent 65f4eae5a9609b7b342a15c0e3c8f40bffb94042 add src diff -r 65f4eae5a960 -r 472b765acb14 midterm.pdf Binary file midterm.pdf has changed diff -r 65f4eae5a960 -r 472b765acb14 midterm.tex --- a/midterm.tex Sun Oct 20 20:15:11 2019 +0900 +++ b/midterm.tex Mon Oct 21 16:18:49 2019 +0900 @@ -61,39 +61,45 @@ \thispagestyle{fancy} \section{研究目的} -当研究室ではOSの信頼性の保証と拡張性の実現のため, CbCを用いた Gears OSの研究を行なっている. -しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. +現代ではOSの信頼性の保証と拡張性の実現が求められている. +%CbCを用いた Gears OSの研究を行なっている. +%しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. %形式手法 -CbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,OS のモデル検査が可能となる． -CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. -本研究ではこれらのことを用い, xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし, OSの信頼性を保証したい. - +%CbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,OS のモデル検査が可能となる． +%CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. +本研究では, CbCのinterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. +また,xv6のinterface実装によりモジュール化が可能となり,拡張性の実現が達成される. %\section{GearsOS} \section{xv6} xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. -xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI-Cに書き換えられ x86 に再実装された. xv6 はシンプルであるがUnixの概念と構造を持っている. +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上で実装されている． - +\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_example.cbc} -\section{CbCのAgdaForm} -%Agdaについて +\section{CbCとAgdaの対応} +Agdaとは定理証明を支援する関数型のプログラミング言語である. +数学の証明に使われる自然演繹と型付きλ計算については対応があり,Agdaでは型付きλ計算を記述する事によって検証することができる. -%Agdaでなぜ説明できるか。飽和ロジック +CbCでは継続を用いてプログラムを記述する.同じくAgdaにも継続の記述方式が存在する.これらの記述は対応している. +以上のことよりCbCをAgdaに書き換える事ができ,CbCで記述されたプログラムはAgdaによって検証することが可能である. %CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー＞ってことを書けば良い？ \section{context} +contextとは一連の実行が行われる際に使用されるCodeGearとDataGearの集合である. +従来のスレッドやプロセスに対応する.Context は接続可能な CodeGear, Data Gear のリスト. Data Gear を確保するメモリ空間,実行される Task への Code Gear 等を持っている. +CodeGearが別のCodeGearに遷移する際,必ずcontextを参照しenumで定義されたCodeGearの番号を指定し遷移する. -%CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し. -%番号で管理している。 +%CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し.enumの番号で管理している。 %dataの保存先と実行するdategearの保存先 %パルスさんの修論 diff -r 65f4eae5a960 -r 472b765acb14 pic/context.graffle Binary file pic/context.graffle has changed diff -r 65f4eae5a960 -r 472b765acb14 src/cbc_example.cbc --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cbc_example.cbc Mon Oct 21 16:18:49 2019 +0900 @@ -0,0 +1,6 @@ +__code cs0(int a, int b){ + goto cs1(a+b); +} +__code cs1(int c){ + goto cs2(c); +}