Mercurial > hg > Papers > 2020 > anatofuz-sigos
changeset 21:7c9cac61b14c
update
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 May 2020 21:31:57 +0900 |
| parents | ca6506bdcda4 |
| children | d933923009db |
| files | etc/xv6model.mm paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex |
| diffstat | 4 files changed, 37 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/etc/xv6model.mm Sat May 02 16:30:15 2020 +0900 +++ b/etc/xv6model.mm Sat May 02 21:31:57 2020 +0900 @@ -76,6 +76,26 @@ </node> </node> </node> +<node CREATED="1588420879127" ID="ID_694783791" MODIFIED="1588420885189" POSITION="right" TEXT="CbC"> +<node CREATED="1588420885528" ID="ID_1718362615" MODIFIED="1588420888713" TEXT="CbCの概要"/> +<node CREATED="1588420889579" ID="ID_94820861" MODIFIED="1588420894077" TEXT="CodeGear"> +<node CREATED="1588420894439" ID="ID_1690545692" MODIFIED="1588420897811" TEXT="軽量継続"/> +<node CREATED="1588420898427" ID="ID_601528707" MODIFIED="1588420902107" TEXT="環境付きgoto"> +<node CREATED="1588420914007" ID="ID_196411479" MODIFIED="1588420920477" TEXT="setjmp/longmp"/> +<node CREATED="1588420920757" ID="ID_469312585" MODIFIED="1588420930536" TEXT="内部コード生成"/> +</node> +<node CREATED="1588420902519" ID="ID_174711025" MODIFIED="1588420912172" TEXT="引数がDataGearに相当する"/> +</node> +<node CREATED="1588420932670" ID="ID_1856809702" MODIFIED="1588420935461" TEXT="GearsOS"> +<node CREATED="1588420938059" ID="ID_458781973" MODIFIED="1588420940008" TEXT="Context"/> +<node CREATED="1588420940358" ID="ID_1211486281" MODIFIED="1588420945634" TEXT="MetaCodeGear"/> +</node> +<node CREATED="1588420935768" ID="ID_1784377971" MODIFIED="1588420962531" TEXT="Data Gear"> +<node CREATED="1588420935972" ID="ID_1752561490" MODIFIED="1588420975142" TEXT="CodeGearの入出力"/> +<node CREATED="1588420975675" ID="ID_627314667" MODIFIED="1588420987865" TEXT="継続を用いてプログラミングする場合は必要"/> +<node CREATED="1588420988358" ID="ID_70353973" MODIFIED="1588421007396" TEXT="グローバルな変数の管理をどうする?"/> +</node> +</node> <node CREATED="1587966144154" ID="ID_1416207432" MODIFIED="1587966148400" POSITION="left" TEXT="目次"> <node CREATED="1587966149328" ID="ID_285261624" MODIFIED="1587966171170" TEXT="OSの信頼性"/> <node CREATED="1587966171873" ID="ID_49224039" MODIFIED="1587966179381" TEXT="XV6 OSの概要"/> @@ -83,5 +103,6 @@ <node CREATED="1587966191026" ID="ID_710119512" MODIFIED="1587966196503" TEXT="CbCの導入"/> <node CREATED="1587966196869" ID="ID_754369000" MODIFIED="1587966199587" TEXT="まとめ"/> </node> +<node CREATED="1588420872286" ID="ID_1472185749" MODIFIED="1588420872286" POSITION="left" TEXT=""/> </node> </map>
--- a/paper/anatofuz-sigos.md Sat May 02 16:30:15 2020 +0900 +++ b/paper/anatofuz-sigos.md Sat May 02 21:31:57 2020 +0900 @@ -16,7 +16,12 @@ しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 -実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。 +さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 +本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。 +ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。 +プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 + +ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 @@ -86,8 +91,8 @@ 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 -これらの状態をまとめる構造体として、 CbCの`context`を導入した。 - +遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 +プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。 # xv6のファイルシステムの一部の分析
--- a/paper/anatofuz-sigos.tex Sat May 02 16:30:15 2020 +0900 +++ b/paper/anatofuz-sigos.tex Sat May 02 21:31:57 2020 +0900 @@ -92,7 +92,12 @@ しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 -実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。 +さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 +本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。 +ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。 +プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 + +ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 @@ -162,8 +167,8 @@ 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 -これらの状態をまとめる構造体として、 CbCの\texttt{context}を導入した。 - +遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 +プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。 \section{xv6のファイルシステムの一部の分析}