Mercurial > hg > Papers > 2019 > menikon-midterm

changeset 18:26c4f49f1dcd

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 Wed, 23 Oct 2019 16:34:03 +0900
parents 66ef03cf117b
children 1f50f5b5e33c
files midterm.pdf midterm.tex
diffstat 2 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
Binary file midterm.pdf has changed
--- a/midterm.tex	Wed Oct 23 15:55:11 2019 +0900
+++ b/midterm.tex	Wed Oct 23 16:34:03 2019 +0900
@@ -60,18 +60,20 @@
 \maketitle
 \thispagestyle{fancy} 
 
-\section{xv6にinterfaceを実装する意味}
+\section{xv6のOSの信頼性保証}
 現代ではOSの信頼性の保証と拡張性の実現が求められている.
 信頼性をノーマルレベルの計算に対して保 証し，拡張性をメタレベルの計算で実現することを目標にContinuation based C (CbC)を用いて Gears OS を設計中である.
-しかし現在は,Gears OSの研究においても様々な問題が存在するため前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている.
+前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている.
 
-CbCにはCodeGear,DataGearという処理の基本的な概念があり,これらを利用する事によってstackに値を積む事なくCodeGear間を遷移することができる.
-そのため,CbCのInterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる.
+CbCにはCodeGearという処理の基本的な単位があり,これらを利用する事によってstackに値を積む事なくCodeGear間を遷移することができる.
+%そのため,CbCのInterfaceを使うとモジュール化ができる.また,
+ stackが無い事によってOS内部の明確化が実現できる.
 %CbCを用いた Gears OSの研究を行なっている.
 %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える.
 %形式手法
 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる．
 %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる.
+CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応している.
 
 これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい.
 また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す.
@@ -125,7 +127,7 @@
 
 %コンテキストには引数置き場所が書いてあるー＞CodeGear
 \section{CbCのInterface}
-CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.%CbCを agdaに対応するために関数プログラミングスタイルで書く事によってInterfaceの検証も可能になる.
+先述した通り, CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.%CbCを agdaに対応するために関数プログラミングスタイルで書く事によってInterfaceの検証も可能になる.
 
 以下の図2は, QueueのInterfaceとSingleLinkedQueueの実装例である.