Mercurial > hg > Document > Growi
changeset 48:a51e6bab65e8
backup 2021-03-17
author | autobackup |
---|---|
date | Wed, 17 Mar 2021 00:10:03 +0900 |
parents | dd41635fe55b |
children | fae0d5b27a2d |
files | trash/user/aosskaito/note/2021/03/16.md trash/user/aosskaito/メモ/2021/03/16.md user/Itsuki/2021/3-16.md user/aosskaito/note/2021/03/16.md user/aosskaito/seminar/2021/03/16.md user/aosskaito/メモ/2021/03/16.md user/matac42/note/2021/03/16.md user/pine/メモ/2021/03/16.md |
diffstat | 8 files changed, 146 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/trash/user/aosskaito/note/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,1 @@ +test \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/trash/user/aosskaito/メモ/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,1 @@ +test \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/Itsuki/2021/3-16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,33 @@ +# 進捗報告 +## 研究目的 +- 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。 + - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。 +- GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。 +- 未実装の機能の一つとしてファイルシステムが挙げられる。 + - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。 + - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。 + - そのためにjavaで構成されているChristieをCbCで構成し直していく。 +- + +> - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。 +> - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。 +> - プログラムの整合性を検査をメタレベルの計算で行いたい。 +> - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。 +> - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。 + + +## 進捗内容 +### サンプルコードの続き +- word_countの続き、金曜日に先生と清水さんにお手伝いしていただいた。 + - https://scrapbox.io/cr-ryukyu/Gears勉強会ログ3%2F12 + - マクロ関係の復習、その他perl部分など + - これからの展望が↓ + - https://scrapbox.io/cr-ryukyu/GearsOSでのWordCount_Pipeline +- DataGearの認識でエラーが発生している状態、perlの処理のバグとりが必要らしい? +- wcのコードを広げて行ってChristieの仕組みを導入する感じ + +## その他の報告 +- 就活のエントリーをしました + - スーツで証明写真撮りに行ったりSPIを忘れてたり + - SPIを数日勉強して受けます。 +- とりあえずはもう1,2社並行に受けておきたい \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/aosskaito/note/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,1 @@ +redirect /trash/user/aosskaito/note/2021/03/16 \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/aosskaito/seminar/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,27 @@ + +# **研究目的** +- 現状未定 + +## 興味あること +- https://mattermost.ie.u-ryukyu.ac.jp/cr-ie-u-ryukyu/pl/5qbbgnn68jb47ekpusak6puopc から気になったのも + - **GearsOS関連** + - まだ関連の論文読めてない + - **リモートエディタ** + - 一木先輩のものを読んでる最中 + - Christie勉強しないとわからなさそう + + - **アプリ開発** + - 改良の方も考えている + +## 調べたこと +- 現在は(https://ie.u-ryukyu.ac.jp/dissertation/entry/34522/)から過去の論文を読んでみている. + +## 調べること +- Christieについて +- GearsOS関連の論文を読んでみる +- vimのundoメカニズム +- vi emacsのトランザクション + +## 趣味関連 +- クトゥルフ神話の原作小説を読もうと思い,H・P・ラヴクラフトの「狂気の山脈にて」を読み始めた. +- 「Stadew Valley」というゲームを最近やっている.1年目の冬で畑ができないので特にやることがない.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/aosskaito/メモ/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,1 @@ +redirect /trash/user/aosskaito/メモ/2021/03/16 \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/matac42/note/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,14 @@ +# 研究目的 + +未定 + + +# やってみたいこと + +データベース関係やってみたい + +* トランザクションとか興味ある + +# Note + +シス管頑張るぞい \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/pine/メモ/2021/03/16.md Wed Mar 17 00:10:03 2021 +0900 @@ -0,0 +1,68 @@ +# 研究目的 + +- 本研究室では、Continuation Based C(CbC)を用いて、信頼性と拡張性を両立するOSであるGearsOSを開発している。 + +- 円滑なOS開発を行うために、GearsOSのデバッガを作成する。 + +## 興味あること +- OS関係 + - カーネル + - ファイルシステム + - プロセス + + +## ゼミlog +https://mattermost.ie.u-ryukyu.ac.jp/cr-ie-u-ryukyu/pl/z5iiphs817f8jpebsf4exnsz7h + +- code gearをdumpするルーチン +- data gearをprintするcode gearを作る +- twiceとかいつきさんの例題をprintする +- どのタイミングでprintするか +- go to metaのとこでprintする +- jumpしてprint +- 関数コールで作ってもいい。これがいい +- data gearは一番上にこれがどうい +- code gearの方法と関数コールの方法 +- stubも + + +- gdbとlldbと同じくらいの機能がほしい +- ↑マルチスレッドどうするか? +- 全部のスレッドを同時にどう止めるか +- signalとp threadのapiがある +- linuxだったらプロセスのシグナルとか +- traceが取れるだけでべんり +- デバッグに必要な機能 +- perl側のデバッガも欲しい + +- 以下の機能が欲しい +- だめな値になった瞬間が知りたい +- 誰のせいでだめになったのか + +- モデル検査のイテレータで任意の地点で再実行する +- いつどこでどんな値に変化されたかdata gearのstate dbが知ってる +- けどプログラムカウンタの前の値は知らない +- 前をたどる機能が欲しい +- そのためにポインタ(reverse pointer)を入れる +- ただし複数考えられるのでリスト形式にする必要がある +- ここもモデル検査のとこ? + +- state DBが複雑 +- これにreverse pointerを入れていいのか? + +- state db自体をdata gearで書きたいけど +- 複雑すぎて無理そう + +- http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/Gears/file/tip/src/parallel_execution/ModelChecking/state_db.h +- state dbは今の所バイナリツリー +- red bra + +- memori.hとstate_db.hをdata gearにする +- 処理をcode gearにする + +- バイナリツリーの処理ルーチンを作る必要がある + +- 最初はサブルーチンで手書きから始める + +- perlの代わりに何でGearsを書くか +- そろそろlanguage independentにしたい