Mercurial > hg > Papers > 2019 > menikon-midterm
changeset 11:566ce65437ea
fix
author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 22 Oct 2019 19:18:30 +0900 |
parents | 9ccfabe96b5d |
children | da87ba72714a |
files | midterm.pdf midterm.tex pic/context.pdf |
diffstat | 3 files changed, 32 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/midterm.tex Mon Oct 21 20:39:04 2019 +0900 +++ b/midterm.tex Tue Oct 22 19:18:30 2019 +0900 @@ -60,16 +60,21 @@ \maketitle \thispagestyle{fancy} -\section{研究目的} +\section{xv6にinterfaceを実装する意味} 現代ではOSの信頼性の保証と拡張性の実現が求められている. +信頼性をノーマルレベルの計算に対して保 証し,拡張性をメタレベルの計算で実現することを目標にContinuation based C (CbC)を用いて Gears OS を設計中である. +しかし現在は,Gears OSの研究においても様々な問題が存在するため前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている. + +CbCにはCodeGear,DataGearという処理の基本的な概念があり,これらを利用する事によってstackに値を積む事なくプロセス間を遷移することができる. +そのため,CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. %CbCを用いた Gears OSの研究を行なっている. %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. +%形式手法 +さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる. +%CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. -%形式手法 -%CbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,OS のモデル検査が可能となる. -%CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. -本研究では, CbCのinterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. -また,xv6のinterface実装によりモジュール化が可能となり,拡張性の実現が達成される. +これらのことを用い,CbCのinterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. +また,xv6のinterface実装によりモジュール化が可能とし,拡張性の実現を目指す. \section{xv6} xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. @@ -79,11 +84,14 @@ xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる. CbC は基本的な処理単位を CodeGearとして定義し,CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する. -以下にCode1にCodeGear遷移時のコード例を示す. +以下のCode1にCodeGear遷移時のコード例を示す. +\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_example.cbc} %図かコードを入れても良いかも + またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ. 現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている. -\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_example.cbc} +今回 ,このCbCに存在するinterfaceをxv6に実装していく. + \section{CbCとAgdaの対応} @@ -98,7 +106,16 @@ \section{context} contextとは一連の実行が行われる際に使用されるCodeGearとDataGearの集合である. 従来のスレッドやプロセスに対応する.Context は接続可能な CodeGear, Data Gear のリスト. Data Gear を確保するメモリ空間,実行される Task への Code Gear 等を持っている. -CodeGearが別のCodeGearに遷移する際,必ずcontextを参照しenumで定義されたCodeGearの番号を指定し遷移する. +CodeGearが別のCodeGearに遷移する際,必ずcontextを参照しenumで定義されたCodeGearの番号を指定し遷移する.ノーマルレベルで見た際のCodeGar,DataGerおよびcontextの関係を以下の図1に簡潔に示す. + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=65mm]{pic/context.pdf} + \end{center} + \caption{CodeGear,DataGear,contxtの関係図} + \label{fig:perl6buil} +\end{figure} + %metaGearの話もした方が良い %CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し.enumの番号で管理している。 @@ -107,10 +124,14 @@ %パルスさんの修論 %コンテキストには引数置き場所が書いてあるー>CodeGear -\section{xv6のinterface} +\section{CbCのinterface} + +\section{xv6のinterfaceのモジュール化} + %呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる. \section{今後の課題} - +先行研究(参考文献[3])によって,xv6のkernelの一部をCbCの特徴でもある継続を用いモジュール化された. +しかし現在では, xv6にinterfaceはまだ搭載されていない.そのため今後, xv6のkernelをinterfaceを用いる事によってどのようにモジュール化できるか考察しながらCbCのinterfaceをxv6に実装していく必要がある. %\begin{thebibliography}{9} \nocite{*}