Mercurial > hg > Papers > 2019 > menikon-midterm

changeset 6:191b3bd3ba1d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author e165723 <e165723@ie.u-ryukyu.ac.jp>
date Sun, 20 Oct 2019 19:28:31 +0900
parents f2089431388b
children db1bf12dcbf7
files midterm.tex pic/context.graffle
diffstat 2 files changed, 9 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- 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の保存先
Binary file pic/context.graffle has changed