Mercurial > hg > Document > Growi
changeset 47:dd41635fe55b
backup 2021-03-10
author | autobackup |
---|---|
date | Wed, 10 Mar 2021 00:10:03 +0900 |
parents | cf7caa17976c |
children | a51e6bab65e8 |
files | user/Itsuki/2021/3-9.md |
diffstat | 1 files changed, 60 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/Itsuki/2021/3-9.md Wed Mar 10 00:10:03 2021 +0900 @@ -0,0 +1,60 @@ +# 進捗報告 +## 研究目的 +- 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。 + - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。 +- GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。 +- 未実装の機能の一つとしてファイルシステムが挙げられる。 + - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。 + - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。 + - そのためにjavaで構成されているChristieをCbCで構成し直していく。 +- + +> - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。 +> - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。 +> - プログラムの整合性を検査をメタレベルの計算で行いたい。 +> - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。 +> - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。 + + +## 進捗内容 +### サンプルコードの続き +- 清水さんにお願いしてWordCount問題の続き + - https://scrapbox.io/cr-ryukyu/Gears勉強会3%2F8ログ + - まだ未完成 + - DataGearの依存関係の問題でコンパイルが失敗している。 + - これを直すには以下の三つのどれか + - wcResultをDataGearでない通常の構造体にする。 + - context.hにDataGearを追加する処理を書き直す。 + - 静的に追加するperlスクリプトの処理を見つけ出す。(あるらしい) +```h + ///Users/ichikitakahiro/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/wc/Wc.h +#ifndef WC_STRUCT + struct Wc { + union Data* wc; + char* filename; + WcResult* result; + enum Code openFile; + enum Code countUp; + enum Code next; + } Wc; +#define WC_STRUCT +#else + struct Wc; +#endif +〜〜略〜〜 +///Users/ichikitakahiro/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/wc/WcResult.h +#ifndef WCRESULT_STRUCT + struct WcResult { + int CountedNum; + char* Keyword; + } WcResult; +#define WCRESULT_STRUCT +#else + struct WcResult; +#endif +``` + +- このDGの問題、清水さんの論文ですでに指摘済みらしい +- 論文読みが足りていないのが明確なので、読みながら書いていく方向で + +## その他の報告