# HG changeset patch # User e165723 # Date 1571567311 -32400 # Node ID 191b3bd3ba1d5884f13d614c005e2c0b0d415df6 # Parent f2089431388bf33d994919261a03263835fd9a0b fix diff -r f2089431388b -r 191b3bd3ba1d midterm.tex --- a/midterm.tex Sun Oct 20 18:29:56 2019 +0900 +++ b/midterm.tex Sun Oct 20 19:28:31 2019 +0900 @@ -61,19 +61,19 @@ \thispagestyle{fancy} \section{研究目的} -現代の OS では拡張性と信頼性を両立させることが要求されている． -信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である． +当研究室ではOSの信頼性の保証と拡張性の実現のため, CbCを用いた Gears OSの研究を行なっている. +しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. %形式手法 +CbC は 定理証明支援系 Agda に置き換えることができるように構築されている. +CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. +本研究ではこれらのことを用い, xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし, OSの信頼性を保証したい. -つまり,CbCのinterfaceを使うとモジュール化とOS内部の明確化がstackなしで実現できる. -本研究ではこれらのことを用い,xv6のinterfaceをCbCで書き換えることによりプロセスごとにkernelの中がどんな状態を保っているかを明確にし,OSの信頼性を保証したい. - -\section{GearsOS} +%\section{GearsOS} \section{xv6} -xv6とはMIT(マサチューセッツ工科大学)のオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. -xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI Cに書き換えられ x86 に再実装された. xv6 はシンプルであるがUnixの概念と構造を持っている. +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言語と互換性のあるプログラミング言語である. @@ -91,6 +91,7 @@ \section{context} + %CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し. %番号で管理している。 %dataの保存先と実行するdategearの保存先 diff -r f2089431388b -r 191b3bd3ba1d pic/context.graffle Binary file pic/context.graffle has changed