annotate paper/anatofuz-sigos.md @ 7:8f1d03a81516

add md2tex
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 30 Apr 2020 13:10:39 +0900
parents
children 92988591be65
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
7
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 # OSの信頼性
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 テスト以外の方法でOSの信頼性を高めたい。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 これに適した形として、 状態遷移モデルが挙げられる。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語で再実装することで仕様の整合性を検証する事が可能である。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 現在小さなunixであるxv6 kernelを状態遷移を基本とした単位でのプログラミングに適した言語、 Continuation Based Cを用いて再実装している。
8f1d03a81516 add md2tex
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 再実装の為には、 既存のxv6 kernelの処理の状態遷移を、継続を用いたプログラムに変換していく必要がある。