Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.md @ 22:d933923009db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Mon, 04 May 2020 11:43:11 +0900
parents 7c9cac61b14c
children 2be09c284a2e
comparison
equal deleted inserted replaced
21:7c9cac61b14c 22:d933923009db
9 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 9 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
10 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。 10 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
11 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 11 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
12 これに適した形として、 状態遷移モデルが挙げられる。 12 これに適した形として、 状態遷移モデルが挙げられる。
13 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 13 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
14 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。 14 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。
15 分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語を用いて再実装することで仕様の整合性を検証する事が可能である。 15 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
16 しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。
17 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 16 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
18 17
19 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 18 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。
20 本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。 19 本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。
21 ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。 20 ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。
29 28
30 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 29 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
31 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 30 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
32 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 31 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
33 32
34 # xv6 kernel
35
36 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
37 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
38 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
39 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
40
41 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
42 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。
43
44 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
45 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。
46 33
47 34
48 # Continuation Based C 35 # Continuation Based C
49 36
50 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 37 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
89 # CbCを用いたOSの実装 76 # CbCを用いたOSの実装
90 77
91 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 78 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
92 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 79 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
93 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 80 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
81 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
82 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。
83
84 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
94 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 85 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
86 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
87 Contextそのものは、 DataGearの実行に必要なMetaDataGearである。
95 プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。 88 プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。
89
90 # xv6 kernel
91
92 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
93 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
94 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
95 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
96
97 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
98 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。
99
100 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
101 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。
96 102
97 103
98 # xv6のファイルシステムの一部の分析 104 # xv6のファイルシステムの一部の分析
99 105
100 xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。 106 xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。