# HG changeset patch # User autobackup # Date 1624374603 -32400 # Node ID c14b8395b5eda6309f203f86faadf7e95b80a2f2 # Parent 1986100619b2de93c126ffa04a2b376533ec0bd5 backup 2021-06-23 diff -r 1986100619b2 -r c14b8395b5ed user/itsuki/2021/6-22.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/itsuki/2021/6-22.md Wed Jun 23 00:10:03 2021 +0900 @@ -0,0 +1,36 @@ +# 進捗報告 +## 研究目的 +- 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。 + - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。 +- GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。 +- 未実装の機能の一つとしてファイルシステムが挙げられる。 + - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。 + - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。 + - そのためにjavaで構成されているChristieをCbCで構成し直していく。 + +> - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。 +> - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。 +> - プログラムの整合性を検査をメタレベルの計算で行いたい。 +> - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。 +> - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。 + + +## 進捗内容 +- またゆーくんとGearsの基本操作の確認してました。 + - 自分も結構忘れてたので思い出しつつ、論文読みつつ + - とりあえずHelloWorldを書いてみた + - いずれhgから消す予定 + - 木曜の18時と土曜朝9時にzoomで一緒にやるように + - 次回はwcあたりを記述していきたい + - もう少しHelloWorldをこねてみてもいいかも + +- 筆記で落ちたと思ってた企業が面接に進んだ + - 一次面接がだいぶ先なので他にもエントリーする予定 + - + +## 雑談 +- 自宅のエアコンが壊れた + - 室外機がぼろくなってガス管を傷つけたのが原因 + - 買い替えが決定 + - 費用は大家さんもちなので助かった + - 「業者は今忙しいからだいぶ先になるよ」と死亡宣告された \ No newline at end of file diff -r 1986100619b2 -r c14b8395b5ed user/matac42/note/2021/06/22.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/matac42/note/2021/06/22.md Wed Jun 23 00:10:03 2021 +0900 @@ -0,0 +1,139 @@ +# 研究目的 + +アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。 + +本研究室では、信頼性に重きを置いたGearsOSを開発している。 + +GearsOSはノーマルレベル、メタレベルの処理を切り分けることができるCbC(Continuation Based C)で記述されている。 + +信頼性とは + +- どのユーザーがどのようなファイル操作をしたかわかること +- logが残ること +- item 操作の辻褄があっていること + +を指す。 + +また、GearsOSには現在未実装の機能があり、その一つにファイルシステムが挙げられる。信頼性を確保するため、ファイルシステムは + +- ファイルシステム全体のトランザクション化 +- ファイルシステム全体のバックアップ\&ロギング + +を取り入れたDataGearManagerとして実装したい。 + +本卒業研究では、GearsOSへファイルシステムの実装を目指す。 + +# GearsOS + +## 例題作成 + +ikkiさんに教えてもらいながらHello, World.やった + +- Headerファイルを作る +- `perl tools/static_gen_header.pl --interface Hello -o examples/helloWorld/Hello.h` +- 実装を書く +- `perl tools/impl2cbc.pl -w examples/helloWorld/HelloImpl.h` +- main.cbcを書く(コピペして編集) +- `CMakeLists.txt`に追記 +- `./cleanup.sh` +- `cmake .` +- `make hello_world` +- `./hello_world` + +### コード + +```c +#include "../../../context.h" +#include +#impl "Hello.h" as "HelloImpl.h" +#interface "Hello.h" +#include + +// ---- +// typedef struct HelloImpl <> impl Hello { +// char* hString; +// char* wString; +// } HelloImpl; +// ---- + +Hello* createHelloImpl(struct Context* context) { + struct Hello* hello = new Hello(); + struct HelloImpl* hello_impl = new HelloImpl(); + hello->hello = (union Data*)hello_impl; + hello->string = NULL; + hello_impl->hString = NULL; + hello_impl->wString = NULL; + hello->h = C_hHelloImpl; + hello->w = C_wHelloImpl; + return hello; +} +__code h(struct HelloImpl* hello, __code next(...)) { + hello->hString = "Hello, "; //createImpl部分では_implなのだが動く + printf("%s", hello->hString); + goto w(hello, next); +} + +__code w(struct HelloImpl* hello, __code next(...)) { + hello->wString = "World.\n"; + printf("%s", hello->wString); + printf("%s\n", hello->hString); + goto next(...); +} +``` + +## 疑問点 + +- cmakeは何をしてるのか + - GearsOSのビルドツール + - automakeに相当 + - automakeはmakeファイルを生成するツール + - CMakeLists.txtはCMakeの設定ファイル + - ビルドしたいプロジェクトで利用するソースコード群を記述する +- cleanup.shは何をしているのか + - cmake関係のファイルを削除している + - cmake_install.cmake + - c + - CMakeFiles + - CMakeCache.txt + - context.h + - build.ninja + - cmakeし直す前に打つ +- Headerファイルとは + - いくつかのファイルで共有の関数宣言やマクロ定義を書く + - #include で呼び出す + - CbCでは + - CGの宣言 + - DGの宣言 +- `#impl "Hello.h" as "HelloImpl.h"` +- generate_stub.pl + - stubCGの生成 + - メタレベルの情報を付け加える + - 拡張子がcのCbCが生成される + - トランスパイラ +- generate_context.pl + - DGの取得 + - CGの取得 +- contextとは + - ContextはCGの軽量継続を行うための環境のようなもの + - CGはCGで環境が閉じていて、CGだけでは他のCGを参照できない + - よって、CGはMCG経由でContextにあるenumをみて次のCGに継続している + - このようにCGを継続させるときにContextを見にいくCGを特にStubCGと呼ぶ +- ループ実装の方針 +- union data + - DGは複数の型になる可能性がある + - どの型でも許容できるようにunion型を用いている + +## memo + +ビルドフロー + +source -> generate_stub.pl -> generate_context.pl -> CbC compiler -> ex file + +## syskan + +podmanにstatic ipを振る方法がわからない + +- https://scrapbox.io/ie-syskan/podmanでfreeradius構築 +- freeradiusのpodmanを作成しようとしている +- ie-webのnetwork設定を見るとmacvlanでやってるっぽい +-