view final_main/chapter1.tex @ 18:18edad46e821

tweak
author menikon
date Thu, 13 Feb 2020 04:06:29 +0900
parents b67e4c9f0374
children a03d74165189
line wrap: on
line source

\chapter{xv6 の OS の信頼性保証}
%\label{chap:introduction}
\pagenumbering{arabic}

%序論の目安としては1枚半ぐらい.
%英語発表者は,最終予稿の「はじめに」の英訳などを載せてもいいかも.

OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C (CbC) を用いて Gears OS を開発中である。前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 を CbC で書き換えている。
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 を使うことで検証や機能の入れ替えによる拡張が可能となる。
本論文では、xv6 の FileSystem をCbCによって書き換えることにより 複雑な処理である FileSystem を明確化させ信頼性を保証、 Interface を使用可能とすることで拡張性を実現することを目標とする。