# HG changeset patch # User Shinji KONO # Date 1588836328 -32400 # Node ID 667ae17b169e26c06b97a06b840609c569da4cb3 # Parent 4cecdfd6b2374c955a467eb0f0a4a43c948ac106 ... diff -r 4cecdfd6b237 -r 667ae17b169e paper/anatofuz-sigos.pdf Binary file paper/anatofuz-sigos.pdf has changed diff -r 4cecdfd6b237 -r 667ae17b169e paper/anatofuz-sigos.tex --- a/paper/anatofuz-sigos.tex Thu May 07 15:40:54 2020 +0900 +++ b/paper/anatofuz-sigos.tex Thu May 07 16:25:28 2020 +0900 @@ -63,58 +63,67 @@ \author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp] \begin{abstract} -OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。 -テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。 - -状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。 -このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。 -本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。 +アプリケーションやサービスの信頼性は、OSと結びついている。OS自身が高い信頼性を持つ必要があり、 +その上で動作するソフトウェアの信頼性をOSが保証するような仕組みがあると良い。 +テストは本質的に有限なケースしか調べないので、テストだけで信頼性を保証するのには限界がある。 +アプリケーションとOSの状態を状態遷移を基本としたモデルに変換しモデル検査やHoare Logic などの形式手法を用いて信頼性を高めたい。 +そのために状態遷移単位での記述に適した継続を基本とした言語であるCbC(Continuation based C)をOSとアプリケーションの記述に用いる。 +最初の段階として小さなunixであるxv6 kernelのCbCによる書き換えを行っている。 +xv6 kernelの処理がどのような状態遷移を行うのかを分析し、CbCの継続ベースでのプログラミングに変換していく必要がある。 +本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析とxv6の書き換えを行う。 \end{abstract} \maketitle -\section{OSの信頼性} -様々なアプリケーションはOSの上で動作するのが当たり前になってきた。 -アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。 -OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。 -しかし並列並行処理などに起因するバグや、 そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 +\section{アプリケーションの信頼性} +アプリケーションの信頼性を向上させるためには、 土台となるOS自体の信頼性が高く保証されていなければならない。 +OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。 +しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 テスト以外の方法でOSの信頼性を高めたい。 -数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 -OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。 +そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 +OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、Agda定理証明支援系\cite{}を利用した証明ベースでの信頼性の確保などの手法が考えられる。 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 -これに適した形として、 状態遷移モデルが挙げられる。 +% これに適した形として、 状態遷移モデルが挙げられる。 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 -既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 +% 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 -さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 -本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。 -ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。 -プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 +OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。 +前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。 +OSはメタ計算を担当していると言える。 +実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが +検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 +ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。 +% プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 +CbCは基本 goto で CodeGaar というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と +呼ばれる隠れた状態を持たない。このため、計算のための情報は CodeGearの入力にすべてそろっている。そのうちのいくつかはメタ計算、 +つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの +区別は入力のどこを扱うかの差に帰着される。 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 -またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 -すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。 +CbCは GCC \cite{}あるいは LLVM \cite{}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 +またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 +% すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 - \section{Continuation Based C} Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。 この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。 -またCbCではこの軽量継続を用いた再帰呼び出しを利用することで\texttt{for}文などのループ文を廃し、 関数型プログラミングに近いスタイルでプログラミングが可能となる。 -現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。 - +またCbCではこの軽量継続を用いて\texttt{for}文などのループ文を実装する。これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。 +実際、Agda よる関数型のCbCの記述も用意されている\cite{}。 +実際のOSやアプリケーションを記述する場合には +GCC及びLLVM/clang上のCbC実装を用いる。 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。