# HG changeset patch # User anatofuz # Date 1588560191 -32400 # Node ID d933923009db8f9b64f27dbd7842e24618fb93a2 # Parent 7c9cac61b14c0e6c5c5b16520e2a3b342a9767a9 ... diff -r 7c9cac61b14c -r d933923009db paper/anatofuz-sigos.md --- a/paper/anatofuz-sigos.md Sat May 02 21:31:57 2020 +0900 +++ b/paper/anatofuz-sigos.md Mon May 04 11:43:11 2020 +0900 @@ -11,9 +11,8 @@ 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 これに適した形として、 状態遷移モデルが挙げられる。 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 -既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。 -分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語を用いて再実装することで仕様の整合性を検証する事が可能である。 -しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。 +既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 +しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 @@ -31,18 +30,6 @@ 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 -# xv6 kernel - -xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 -xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 -Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 -本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 - -xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 -またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 - -本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 -xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 # Continuation Based C @@ -91,9 +78,28 @@ 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 +CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 +CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 + +GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 +このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 +Contextそのものは、 DataGearの実行に必要なMetaDataGearである。 プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。 +# xv6 kernel + +xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 +xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 +Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 +本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 + +xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 +またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 + +本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 +xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 + # xv6のファイルシステムの一部の分析 diff -r 7c9cac61b14c -r d933923009db paper/anatofuz-sigos.pdf Binary file paper/anatofuz-sigos.pdf has changed diff -r 7c9cac61b14c -r d933923009db paper/anatofuz-sigos.tex --- a/paper/anatofuz-sigos.tex Sat May 02 21:31:57 2020 +0900 +++ b/paper/anatofuz-sigos.tex Mon May 04 11:43:11 2020 +0900 @@ -87,9 +87,8 @@ 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 これに適した形として、 状態遷移モデルが挙げられる。 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 -既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。 -分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語を用いて再実装することで仕様の整合性を検証する事が可能である。 -しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。 +既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 +しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 @@ -107,18 +106,6 @@ 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 -\section{xv6 kernel} - -xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 -xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 -Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 -本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 - -xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 -またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 - -本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 -xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 \section{Continuation Based C} @@ -167,9 +154,28 @@ 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 +CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 +CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 + +GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 +このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 +Contextそのものは、 DataGearの実行に必要なMetaDataGearである。 プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。 +\section{xv6 kernel} + +xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 +xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 +Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 +本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 + +xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 +またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 + +本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 +xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 + \section{xv6のファイルシステムの一部の分析}