Mercurial > hg > Papers > 2020 > menikon-thesis
view final_main/chapter1.tex @ 30:10bdabd06497 default tip
fix
author | menikon |
---|---|
date | Mon, 17 Feb 2020 04:52:15 +0900 |
parents | d4c7ffd507a3 |
children |
line wrap: on
line source
\chapter{OS に対する信頼性の保証} %\label{chap:introduction} \pagenumbering{arabic} OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C\cite{cbc}(CbC)を用いて Gears OS\cite{gears}を開発中である。 CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、stack に値を積む事なく CodeGear 間を遷移することができる。% stack が無い事に よって OS 内部の明確化が実現できる。 Code Gear に対して入力の Data Gear と 出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。 CbC の Interface は Gears OS のモジュール化の仕組みである。この Interface は、Java の Interface や Haskell の型クラスに対応し、導入することで仕様と実装に分けて記述することが出来る。Interface を使うことで検証や機能の入れ替えによる拡張が可能となる。 前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 \cite{xv6} を CbC で書き換えている。 本論文では、xv6 の FileSystem をCbCによって書き換えることにより 複雑な処理である FileSystem を明確化させ信頼性を保証、 Interface を使用可能とすることで拡張性を実現することを目標とする。