|
2
|
1 \chapter*{要旨}
|
|
33
|
2 OS 自体に信頼性が求められるが、OS の全てのコードに対して検証を行うのは困難である。
|
|
14
|
3
|
|
33
|
4 本研究室で信頼性を保障するのに適したプログラミング言語 CbC を開発してきた。
|
|
|
5 CbC を使って OS の開発をすることにより、
|
|
|
6 CbC の軽量継続によりOSの動作を
|
|
|
7 状態遷移を基本としたモデルに落とし込むことができる。
|
|
|
8 これにより状態遷移機械の検証手法をOSに対して適用し信頼性を高めることができるようになると考えられる。
|
|
42
|
9 本研究では小型のOSであるxv6 をCbCで書き換えること
|
|
33
|
10 の一部を行う。具体的にはOSのメモリ管理を担当するvm.cをCbCに変換する。
|
|
14
|
11
|
|
33
|
12 CbCではインターフェースを用いたモジュール化を行う。
|
|
|
13 vm.cbcはメモリ管理(特にpaging)を行うインターフェース
|
|
|
14 と、その実装として記述される。インターフェース内部での
|
|
|
15 CbCの接続はメタレベルの記述になる。OSで使われる
|
|
|
16 すべてのコードとデータはcontextと呼ばれるメタデータ
|
|
|
17 に記述される。contextのデータを書き換えることにより
|
|
|
18 、x.v6で仮想OSやコンテナを定義できるようになると
|
|
|
19 考えられる。
|
|
14
|
20
|
|
33
|
21 本論文では
|
|
|
22 OSの信頼性の基本であるメモリ管理部分のインターフェースと実装の記述の考察を行う。
|
|
13
|
23
|
|
|
24 % 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装しているが、
|
|
2
|
25
|
|
|
26 \chapter*{Abstract}
|
|
33
|
27 Reliability of Operating Systems are important,
|
|
|
28 but it is difficult to verify the source code of
|
|
|
29 the Operating System.
|
|
|
30
|
|
|
31 Programming language CbC is developed in our laboratory,
|
|
|
32 which is designed to support reliability.
|
|
|
33 Operating System Project has
|
|
|
34 automaton like descriptions if it is written in CbC.
|
|
|
35 Using automaton based verification technologies,
|
|
|
36 the Operating System becomes more dependable.
|
|
|
37 In this research, we will rewrite x.v6 kernel which
|
|
|
38 is a small operating system written in C. Actually,
|
|
|
39 we will rewrite the memory management part vm.c of it using CbC.
|
|
|
40
|
|
|
41 CbC has module system called interfaces. vm.cbc is
|
|
|
42 implemented as an interface and the implementations.
|
|
|
43 In the interfaces, all connections and data structures
|
|
|
44 are written a meta data, which is called Context.
|
|
|
45 Virtual OS or so called Container can be realized as
|
|
|
46 a modification of the Context.
|
|
|
47
|
|
|
48 In this paper, we describes rewriting details of
|
|
|
49 memory management interface.
|
|
14
|
50
|
|
|
51
|
|
33
|
52
|
|
|
53
|
|
15
|
54
|
|
33
|
55
|
|
|
56
|
