|
23
|
1 \chapter{OSとアプリケーションの信頼性}
|
|
2
|
2
|
|
|
3 コンピューター上では様々なアプリケーションが常時動作している。
|
|
|
4 動作しているアプリケーションは信頼性が保証されていてほしい。
|
|
|
5 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
|
|
|
6 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。
|
|
|
7
|
|
29
|
8 実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。
|
|
2
|
9 OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。
|
|
|
10 OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。
|
|
|
11 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
|
|
|
12 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
|
|
|
13 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
|
|
|
14 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。
|
|
|
15
|
|
15
|
16
|
|
65
|
17 テストコード以外の方法として、 形式手法と呼ばれるアプローチがある。
|
|
56
|
18 形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
|
|
30
|
19 証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
|
|
15
|
20 Curry-Howard同型対応則により、型と論理式の命題が対応する。
|
|
|
21 この型を導出するプログラムと実際の証明が対応する。
|
|
30
|
22 証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
|
|
|
23 整合性の確認は、記述した関数を元に定理証明支援系が検証する。
|
|
15
|
24 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
|
|
|
25 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
|
|
65
|
26 検証されたアルゴリズムをもとにCで実装することは可能であるが、 移植時にバグが入る可能性がある。
|
|
15
|
27 検証ができているソースコードそのものを使ってOSを動作させたい。
|
|
|
28
|
|
|
29
|
|
|
30 他の形式手法にモデル検査がある。
|
|
55
|
31 モデル検査はプログラムの可能な実行をすべて数え上げて要求している使用を満たしているかどうかを調べる手法である。
|
|
23
|
32 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
|
|
15
|
33 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
|
|
23
|
34 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
|
|
26
|
35 しかしOSの処理は膨大である。
|
|
|
36 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
|
|
|
37 状態を有限に制限したり抽象化を行う必要がある。
|
|
60
|
38 また、モデル検査ができるモデル検査器は特定のプログラム形式でないと動かないものがある。
|
|
|
39 例えばSpinはPromela形式でないとモデル検査ができない。
|
|
|
40 モデル検査ができる場合も、 モデル検査したコードと実際に動くコードを同一にしたい。
|
|
|
41 また、モデル検査をする場合としない場合の切り替えを、より手軽に行いたい。
|
|
23
|
42
|
|
|
43
|
|
|
44 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
|
|
|
45 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
|
|
|
46 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
|
|
|
47 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
|
|
30
|
48 この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel}
|
|
|
49 証明しやすい表現の例として、 状態遷移ベースでの実装がある。
|
|
23
|
50
|
|
|
51
|
|
24
|
52 証明を行う対象の計算は、 その意味が大きく別けられる。
|
|
|
53 OSやプログラムの動作においては本来したい計算がまず存在する。
|
|
|
54 これはプログラマが通常プログラミングするものである。
|
|
28
|
55 これら本来行いたい処理のほかに、 CPU、メモリ、スレッドなどの資源管理なども必要となる。
|
|
|
56 前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
|
|
|
57 OSはメタ計算を担当していると言える。
|
|
26
|
58 ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。
|
|
32
|
59 システムコールを呼び出すとOSが管理する資源に対して何らかの副作用が発生するメタ計算と言える。
|
|
|
60 副作用は関数型プログラムの見方からするとモナドと言え、 モナドもメタ計算ととらえることができる。
|
|
|
61 OS上で動くプログラムはCPUにより並行実行される。この際の他のプロセスとの干渉もメタレベルの処理である。
|
|
28
|
62 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
|
|
|
63 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
|
|
26
|
64 ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。
|
|
|
65
|
|
|
66
|
|
|
67 プログラムの整合性の検証はメタレベルの計算で行いたい。
|
|
24
|
68 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
|
|
|
69 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
|
|
60
|
70 この場合は検証を実行するメタ計算と、 検証をしないメタ計算を手軽に切り替える必要がある。
|
|
65
|
71 さらに検証用とそうでない用で、動作させたいアルゴリズムの実装そのもののコードを変更したくない。
|
|
|
72 これも検証をメタレベルで行い、実装をノーマルレベルで行い、各レベルを切り離すことで実現可能である。
|
|
24
|
73 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
|
|
65
|
74 ノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。
|
|
24
|
75
|
|
28
|
76 プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。
|
|
32
|
77 CbCは基本\texttt{goto文}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と呼ばれる隠れた状態を持たない。
|
|
|
78 このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。
|
|
|
79 そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(\texttt{DataGear})である。
|
|
28
|
80 メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
|
|
32
|
81 CbCはCと互換性のあるCの下位言語である。
|
|
28
|
82 CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
|
|
32
|
83 Cのコンパイルシステムを使える為に、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
|
|
|
84 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
|
|
65
|
85
|
|
|
86 CbCを用いてノーマルレベルとメタレベルの分離を行い、信頼性と拡張性を両立させることを目的としてGearsOSを開発している。
|
|
|
87 GeasOSでは、 CbCの実行単位であるCodeGearとデータの単位であるDataGearを基本単位としている。
|
|
|
88 GearsOSのメタ計算にはMetaCodeGearとMetaDataGearを用いる。
|
|
|
89 信頼性の保証はMetaCodeGearで行いたい。
|
|
|
90 その為にはGearsOSが柔軟にメタ計算を切り替えることが必要となる。
|
|
|
91 また、GearsOSで実行されるメタ計算の数は膨大である。
|
|
|
92 すべてをプログラミングするのではなく、いくつかのメタ計算は自動で生成されてほしい。
|
|
|
93 GearsOSでは拡張性の保証も重要な課題である。
|
|
|
94 拡張性を保証するにはすべて純粋なCbCで実装すると、実装がきわめて煩雑である。
|
|
|
95 その為にはCbCとセマンティックが等しいより簡潔なGearsOS独自のシンタックスなどが必要である。
|
|
91
|
96 独自のシンタックスはPerlスクリプトによって等価なCbCのソースコードに変換していた。
|
|
|
97
|
|
|
98 従来のPerlスクリプトによるソースコードの変換では、 CodeGearが出力をDataGearに書き出す際に、 手でメタ計算を書かなければならない問題があった。
|
|
|
99 また、 GearsOSのモジュール化の仕組みであるInterfaceの実装であるImplementの型定義ファイルが存在していなかった。
|
|
|
100 GearsOSではノーマルレベルで宣言したDataGearは、構造体の形で表現される。
|
|
|
101 従来のシステムではこの構造体も手で実装しなければならず、メタレベルの計算のうち大半を手で実装する必要があった。
|
|
|
102 これらのメタレベルの計算はコンパイル時に決定するために、自動化を行いたい。
|
|
65
|
103
|
|
|
104 本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察する。
|
|
91
|
105 GearsOSがメタ計算を自動生成しているPerlトランスパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。 |
