# HG changeset patch
# User autobackup
# Date 1619536203 -32400
# Node ID 1e901cd5370fa3e73d2bd9c49aef3af3f95ecba3
# Parent  afba7141d1a6d2b5fa958ae5be48e533b4ca7efc
backup 2021-04-28

diff -r afba7141d1a6 -r 1e901cd5370f user/Itsuki/2021/4-27.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/Itsuki/2021/4-27.md	Wed Apr 28 00:10:03 2021 +0900
@@ -0,0 +1,35 @@
+# 進捗報告 
+## 研究目的
+- 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。
+    - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。
+- GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。
+- 未実装の機能の一つとしてファイルシステムが挙げられる。
+    - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。
+    - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。
+    - そのためにjavaで構成されているChristieをCbCで構成し直していく。 
+
+> - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。
+>     - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。
+>     - プログラムの整合性を検査をメタレベルの計算で行いたい。
+>     - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。
+> - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。
+
+
+## 進捗内容
+- MindMapを書いてみました
+    - 自分で書くべきではと思うところを書き出してみた。
+- WordCountについて
+    - FileOpen部分は他APIを書く際ことを考えて簡略化(メタに隠蔽)したい。
+        - open時のモードどうする？
+        - openしたらバッファも作るようにしておく
+    - ???元のスレッドにCGの結果を返すにはpar gotoを使う
+        - par gotoはgearsの分散処理の際に使用する。
+        - par gotoでGearboxに近いことが実装できる？
+    - 処理途中でエラーを吐いたらエラー用のCGにgotoする。
+- 
+
+
+## その他の報告
+- 面接1社目祈られました。
+    - GearsOSの話したら「すごいことやってんねぇ」と言われた。
+    - OSいじってる学生はわりと珍しいらしい。
\ No newline at end of file
diff -r afba7141d1a6 -r 1e901cd5370f user/pine/note/2021/04/27.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/2021/04/27.md	Wed Apr 28 00:10:03 2021 +0900
@@ -0,0 +1,15 @@
+# 研究目的
+- アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。
+
+- 本研究室では、Continuation Based C(CbC)を用いて、信頼性と拡張性を両立するOSであるGearsOSを開発している。
+
+- ソフトウェア開発においてエラー・バグは付き物であり、その発見が重要である。現在GearsOSにはデバッガーが未実装であるため、円滑なOS開発を行うために、GearsOSのデバッガーを作成する。
+
+## やったこと
+- アナグラさんの論文を呼んでいる途中
+- 活動計画を書いた
+
+
+## やること
+- 先輩のGearsの論文を見る
+- Gears, CbCを動かしてみる
\ No newline at end of file
diff -r afba7141d1a6 -r 1e901cd5370f user/soto/log/2021-04-20.md
--- a/user/soto/log/2021-04-20.md	Sat Apr 24 00:10:04 2021 +0900
+++ b/user/soto/log/2021-04-20.md	Wed Apr 28 00:10:03 2021 +0900
@@ -21,9 +21,6 @@
 
 - モデル検査について調べていた
 
-- LLVMについても勉強したかった
-    - 「きつねさんでもわかるLLVM」を読んでいたが、難しくて寝てしまった(つまり僕の理解力はきつねさん以下だった…)
-
 - Gears Agdaで Red Black Tree を作成する
     - 卒論時に作成していたものを修正するなどしていた
         - deleteの部分に実は上手くできていない所があったのでリファクタリングをしています…
@@ -44,13 +41,10 @@
     - [Agda プラグイン機構](https://www.jstage.jst.go.jp/article/jssstconference/22/0/22_0_507/_pdf/-char/ja)
     - [NuSMVによるモデル検査入門 (1)](https://qiita.com/shinsa82/items/cd4d95c616bf1da852ce)
 
-## LLVMについても勉強したかった
-- 「きつねさんでもわかるLLVM」を読んでいたが、難しくて寝てしまった(つまり僕の理解力はきつねさん以下だった…)
 
 ## 今後やりたい事/やらないといけない事
-- RustはLLVMで出来ている
-    - ので、LLVM側に Continuation Style を適応出来たら嬉しい
-
+- while loopの検証
+- 
 - 研究計画書
     - なぜかアナウンスがまるでない…