annotate paper/text/introduction.tex @ 56:e55a4d44423c default tip

...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Thu, 17 Feb 2022 19:53:47 +0900
parents 8fbd88035545
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
45
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
1 \chapter{GearsOSにおけるFile system}
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
2
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
3 アプリケーションの信頼性を保証することは
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
4 情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
5 アプリケーションの信頼性を保証するために,基盤となるOSの信頼性を高める必要がある.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
6
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
7 当研究室では,信頼性の保証を目的としたGearsOSを開発している.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
8 OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
9 当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており,
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
10 ノーマルレベルとメタレベルを簡単に切り分けることを可能としている.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 CbCでメタレベルの処理を切り出したものに対して,定理証明やモデル検査を行うことで信頼性を保証する.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13 GearsOSは現在OSとして重要な機能がいくつか未実装であり,言語フレームワークのように動作している状態である.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
14 未実装の機能の一つとしてファイルシステムが挙げられる.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
15 ファイルシステムはファイルやディレクトリといった構造を持ち,データの保存,整理を行う.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
16 また,OSが管理するデータの操作を人間が行いやすいようにinterfaceを提供する.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
17 OSの機能の中でも特に重要な機能であるため,GearsOSにも実装を行う必要がある.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
18
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
19 今回GearsOSへファイルシステムを実装するにあたり,Unixのファイルシステムを参考にする.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
20 Unixのファイルシステムではファイルのメタデータをinodeの形式で保持している.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
21 同様にinodeの仕組みを用いてGearsOSのファイルシステムを実装を行いたい.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
22 interfaceについても,cd,ls,mkdirというようにUnix likeに実装したい.
46
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
23 当研究室ではxv6のCbCでの書き換えを行なっているが,今回はxv6のルーチンをCbCで書き換えるのではなく
45
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
24 GearsOSへUnixのFile systemの仕組みを取り入れるアプローチをとりたい.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
25 それはGearsOSとCbCで書き換えたxv6の比較や,
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
26 互いにファイルシステムの機能の移植が行える様にするためである.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
27 また,当研究室で開発している分散フレームワークChristieの仕組みを用いて,分散ファイルシステムを実装したい.
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
28
d40d5c4e392f fix introduction
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
29 本論文ではGearsOSのファイルシステムに関する基礎概念と,ファイルシステムの構築について記述する.