# HG changeset patch # User autobackup # Date 1634656204 -32400 # Node ID edf8ac727c05f4d1f989b90060cf1a24276fcd29 # Parent d3c9934a0b4b020b639f60e961a4014dd4a68d36 backup 2021-10-20 diff -r d3c9934a0b4b -r edf8ac727c05 user/matac42/note/2021/10/19.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/matac42/note/2021/10/19.md Wed Oct 20 00:10:04 2021 +0900 @@ -0,0 +1,51 @@ +# 研究目的 + +アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。 + +本研究室では、信頼性に重きを置いたGearsOSを開発している。 + +GearsOSはノーマルレベル、メタレベルの処理を切り分けることができるCbC(Continuation Based C)で記述されている。 + +信頼性とは + +- どのユーザーがどのようなファイル操作をしたかわかること +- logが残ること +- item 操作の辻褄があっていること + +を指す。 + +また、GearsOSには現在未実装の機能があり、その一つにファイルシステムが挙げられる。信頼性を確保するため、ファイルシステムは + +- ファイルシステム全体のトランザクション化 +- ファイルシステム全体のバックアップ\&ロギング + +を取り入れたDataGearManagerとして実装したい。 + +本卒業研究では、GearsOSへファイルシステムの実装を目指す。 + +# Gears + +rbtreeを使うコードを書いていた。 + +tree->putがcheckAndSetAtomicReferenceを向いてしまっている + +```sh +(lldb) p tree->put +(Code) $7 = C_checkAndSetAtomicReference +``` + +`tree->put = Gearef(context, Tree)->put`とかでは特に変わらなかった... + +```c +__code putDataTest(struct Context *context,struct Tree* tree) { + printf("put\n"); + Node* node = &ALLOCATE(context, Node)->Node; + node->key = 0; + node->value = (union Data*) createSynchronizedQueue(context); + Gearef(context, Tree)->tree = (union Data*) tree; + Gearef(context, Tree)->node = node; + Gearef(context, Tree)->next = C_printResult; + tree->put = Gearef(context, Tree)->put; + goto meta(context, tree->put); +} +``` \ No newline at end of file diff -r d3c9934a0b4b -r edf8ac727c05 user/pine/note/2021/10/19.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/pine/note/2021/10/19.md Wed Oct 20 00:10:04 2021 +0900 @@ -0,0 +1,149 @@ +# 研究目的 +- アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。 + +- 本研究室では、Continuation Based C(CbC)を用いて、信頼性と拡張性を両立するOSであるGearsOSを開発している。 + +- ソフトウェア開発においてエラー・バグは付き物であり、その発見が重要である。現在GearsOSにはデバッガーが未実装であるため、円滑なOS開発を行うために、GearsOSのデバッガーを作成する。 + +## やったこと +- 実行時に`-debug`オプションを指定できるようにした。 +- プロンプトの実装 + +## 作業ログ +DPPMCのmain.cbc内のinit()で`-debug`オプションを受け取れる用に変更。 +``` +void init(int argc, char** argv) { + for (int i = 1; argv[i]; ++i) { + if (strcmp(argv[i], "-cpu") == 0) + cpu_num = (int)atoi(argv[i+1]); + else if (strcmp(argv[i], "-cuda") == 0) { + gpu_num = 1; + CPU_CUDA = 0; + } else if (strcmp(argv[i], "-debug") == 0) { + printf("get -debug option in main function\n"); + DEBUG_OPTION = 1; + } + } +} +``` + +また、mcMetaのgoto先を`-debug`オプションの有無で変更している。 +``` + if (DEBUG_OPTION == 0) { + printf("DEBUG_OPTION: %i, goto meta\n", DEBUG_OPTION); + goto meta(context, context->next); + } else { + printf("DEBUG_OPTION: %i, goto debug\n", DEBUG_OPTION); + goto debugMeta(context, context->next); + } +``` + +`./DPPMC`で実行すると、通常のModelCheckingが行われる。 + +`./DPPMC -debug`で実行すると、debugMetaにgotoされる。 + +debugMeta内でプロンプトの表示を行っている。 + +また、プロンプトの入力によって異なる処理をさせるようにしている。 + +``` +__ncode debugMeta(struct Context* context, enum Code next) { + context->next = next; // remember next Code Gear + + while(1) { + char user_input_buffer[256]; + size_t length; + + printf("-----------------------\n\n"); + printf("(Gears Debugger) "); + + // delete new line + fgets(user_input_buffer, 256, stdin); + length = strlen(user_input_buffer); + if (user_input_buffer[length - 1] == '\n') { + user_input_buffer[--length] = '\0'; + } + + printf("user_input: %s\n", user_input_buffer); + + if (strcmp(user_input_buffer, "n") == 0) { + goto meta(context, context->next); + } else if (strcmp(user_input_buffer, "q") == 0) { + printf("quit program\n"); + exit(0); + } else if (strcmp(user_input_buffer, "pd") == 0){ + // TODO: create and call CodeGear for print DataGear + printf("print DataGear\n"); + printf("DataGear Address: %p\n", context->data); + printf("Phils\n"); + printf("putdown_lfork: %i\n", context->data[D_Phils]->Phils.putdown_lfork); + printf("putdown_rfork: %i\n", context->data[D_Phils]->Phils.putdown_rfork); + printf("thinking: %i\n", context->data[D_Phils]->Phils.thinking); + printf("pickup_lfork: %i\n", context->data[D_Phils]->Phils.pickup_lfork); + printf("pickup_rfork: %i\n", context->data[D_Phils]->Phils.pickup_rfork); + printf("eating: %i\n", context->data[D_Phils]->Phils.eating); + printf("next: %i\n", context->data[D_Phils]->Phils.next); + } else { + printf("invalid input\n"); + continue; + } + } +} +``` + +`n`を入力すると、次の処理を行う。 +``` +(Gears Debugger) n +user_input: n +ffffffff ffffffff ffffffff ffffffff 04000000 46000000 01000000 46000000 46000000 46000000 flag 0 0x7fcff4d043a0 -> 0x7fcff4d04610 hash b385a087 iter 5 +DEBUG_OPTION: 1, goto debug +----------------------- + +(Gears Debugger) n +user_input: n +4: eating +04000000 ffffffff ffffffff ffffffff 04000000 46000000 2a000000 46000000 46000000 46000000 flag 0 0x7fcff4d04610 -> 0x7fd10b405bd0 hash 2235d9fd iter 5 +DEBUG_OPTION: 1, goto debug +----------------------- +``` + +`pd`を入力すると、DataGearの表示を行う。 + +なお現状はPhilsの型とかをハードコーディングしてるので、Philsの表示しかできないが、今後Impl名などを指定して出せるようにしたい。 +``` +(Gears Debugger) pd +user_input: pd +print DataGear +DataGear Address: 0x7fca0b400000 +Phils +putdown_lfork: 0 +putdown_rfork: 0 +thinking: 0 +pickup_lfork: 0 +pickup_rfork: 0 +eating: 0 +next: 10 +----------------------- +``` + +`q`を入力すると、プログラムを終了する。 +``` +(Gears Debugger) q +user_input: q +quit program +``` + +現状は`n`, `pd`, `q`の3種類のみを実装している。 + +中間報告提出まであと10日くらいなのでそれくらいで終わるのをやりたい。 + +## やること +- プロンプトで名前を指定してDataGearの表示 +- CodeGearの表示 +- ブレークポイントを設定できるようにする +- backtrace, forwardtraceの実装 +- 変数の変更が誰によって行われたかがわかるようにする。 + +## その他 + + diff -r d3c9934a0b4b -r edf8ac727c05 user/soto/log/2021-10-19.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/soto/log/2021-10-19.md Wed Oct 20 00:10:04 2021 +0900 @@ -0,0 +1,41 @@ +# 研究目的 + +愚直にプログラムを書くと、冗長なコードができてしまい、 +実行時間も掛かってしまう + +この場合、コードに対してアルゴリズムを適応すると、 +実行が最適化され実行時間が減り、良いコードが作成できる + +しかし、世の中にはアルゴリズムが大量にあり、 +これを一人で全て覚え、また適応できる場面を思いつくというのは困難 + +そのため、人が愚直に書いたコードに対してアルゴリズムを使用するコードに +自動適用できるようにしたい（すでにあるかもしれないが） + +適用前と適用後で同じコードになっていることを +保障するのは難しい。 + +また、普通のプログラミング言語では、関数の遷移が +自由であるため、これを行うのは難しいと考える + +これによりGears Agdaにて書いたコードをアルゴリズムで +書いたコードに変更 + +# 今やっている研究の目的 + +- OS やアプリケーションの信頼性を高めることは重要な課題である。 +- 信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。 +- 具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。 +- 当研究室では Continuation based C (CbC) という言語を開発している。 + - CbC とは、 C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C 言語の下位言語である。その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。 +- 検証には定理証明を用いるため、 定理証明支援器のAgda を用いる。 +- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う + +# 進捗 + +- 卒論の際に Gears Agda で書いた left learning red black tree を reb black tree に書き直しています。 + + + + +