Mercurial > hg > Papers > 2019 > menikon-midterm
comparison midterm.tex @ 20:bfc913ee4393 default tip
fix
author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 23 Oct 2019 16:42:53 +0900 |
parents | 1f50f5b5e33c |
children |
comparison
equal
deleted
inserted
replaced
19:1f50f5b5e33c | 20:bfc913ee4393 |
---|---|
71 %CbCを用いた Gears OSの研究を行なっている. | 71 %CbCを用いた Gears OSの研究を行なっている. |
72 %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. | 72 %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. |
73 %形式手法 | 73 %形式手法 |
74 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる. | 74 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる. |
75 %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. | 75 %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. |
76 CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり,そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.そのため,CbCのInterfaceを使うとモジュール化ができる. | 76 CbCのInterface は Gears OS のモジュール化の仕組みである. このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.そのため,CbCのInterfaceを使うとモジュール化ができる. |
77 | 77 |
78 これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. | 78 これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. |
79 また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す. | 79 また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す. |
80 | 80 |
81 \section{xv6} | 81 \section{xv6} |