# HG changeset patch # User anatofuz # Date 1588422717 -32400 # Node ID 7c9cac61b14c0e6c5c5b16520e2a3b342a9767a9 # Parent ca6506bdcda42cad6a877d7da9ec0b146f075843 update diff -r ca6506bdcda4 -r 7c9cac61b14c etc/xv6model.mm --- 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 @@ + + + + + + + + + + + + + + + + + + + + @@ -83,5 +103,6 @@ + diff -r ca6506bdcda4 -r 7c9cac61b14c paper/anatofuz-sigos.md --- 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のファイルシステムの一部の分析 diff -r ca6506bdcda4 -r 7c9cac61b14c paper/anatofuz-sigos.pdf Binary file paper/anatofuz-sigos.pdf has changed diff -r ca6506bdcda4 -r 7c9cac61b14c paper/anatofuz-sigos.tex --- 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のファイルシステムの一部の分析}