--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2021/04/20.md	Wed Apr 21 00:10:03 2021 +0900
@@ -0,0 +1,69 @@
+# 研究目的
+
+アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある
+
+本研究室では、信頼性に重きを置いたGearsOSを開発している
+  * GearsOSはノーマルレベル、メタレベルの処理を切り分けることができCbC(Continuation Based C)で記述されている
+
+信頼性とは
+  * どのユーザーがどのようなファイル操作をしたかわかる、logが残る
+  * 操作の辻褄があっている
+
+CbCには
+  * main.cbcなどにユーザーレベルから見えなくても良いコードがある
+      * 隠したい
+
+GearsOSには現在、未実装の機能がある
+  * ファイルシステム
+      * ファイルシステム全体をトランザクションにしたい
+      * ファイルシステム全体のバックアップをとりたい
+  * リンカ
+      * ライブラリとの接続
+      * OS自体にリンカを実装したい
+          * (まだよくわかってない)
+
+ファイルシステムを並列分散処理フレームワークChristieで実装する
+
+# 活動
+
+itsukiさんのwc関連のzoomにお邪魔した
+
+自分のlocalで例題をbuild出来なかったのを解決した
+- cmakeのバージョンがずれたのが原因だった
+- `cmake .`やり直して、cmakeのバージョンを反映させたら治った
+
+Gears関連でやるべきことをなど聞いた
+- ユーザーレベルで見えなくても良いものを隠す
+- リンカ
+- モデル検査
+- 論文読もう
+    - xv6
+        - Uさん
+        - menikonさん
+        - attonさん
+        - parusuさん
+
+把握したこと
+- Codegear, Datagearが入ってるのがcontext
+- Wcの実装がWcImpl
+- wcのopenfileとcountupを分離したい
+- CbC -> perlでの変換 -> C(メタ)
+- makeでperlでの変換とコンパイルする
+
+# シス管
+
+ミーティングが週2になった
+
+もしかしたら台風が来るかもしれないのでidracの確認とかした(台風それてる...?)
+
+Radiusがどこで動いているかアナグラさんに聞いてわかった
+
+b2のtakumi君と作業した
+
+# その他
+
+ディスプレイ選定中...たくさんあるなぁ
+
+30日に活動計画書（計画部分）を書いて提出する必要がある
+
+バイト先がReact使ってるのでReact勉強
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/2020/04/20.md	Wed Apr 21 00:10:03 2021 +0900
@@ -0,0 +1,18 @@
+# 研究目的
+- アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。
+
+- 本研究室では、Continuation Based C(CbC)を用いて、信頼性と拡張性を両立するOSであるGearsOSを開発している。
+
+- 現在GearsOSにはデバッガーが未実装であるため、円滑なOS開発を行うために、GearsOSのデバッガーを作成する。
+
+## やったこと
+- CbCとGearsの環境構築の途中
+
+
+## やること
+- OSのデバッガがどんなものか調べる
+- 先輩のGearsの論文を見る
+- 例題を書いてみる
+- 活動計画書を書く
+    - 4/30締め切り
+    - 今週中に書いて来週のゼミで確認してもらう
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/riono210/seminar/202104/0420.md	Wed Apr 21 00:10:03 2021 +0900
@@ -0,0 +1,34 @@
+## mmdd
+
+## 研究目的
+* ゲームの通信方式にはクライアントサーバ方式とp2p方式がある
+* データの安全性やチート対策などでクライアントサーバ方式が主流
+* サーバに接続してマルチプレイなどのデータ同期を実現させているため、低速
+* 高速かつ安全に通信を行たい
+    * 並列分散フレームワークChristieがある
+    * Christieを利用してp2pで通信を行う
+* ゲーム開発で主に使用されているUnityに対応するためにChristieをC#へ書き換えを行う
+
+## 今週の進捗
+* Socket周りを改修中です
+    * ipAddressAnyに対応させた
+    * やっぱり一筋縄では行かなそう
+
+
+#### IpAddressAny
+
+```
+TcpListener listener = new TcpListener(IPAddress.IPv6Any, localPort);
+// listen on any address ipv4/ipv6
+listener.Server.SetSocketOption(SocketOptionLevel.IPv6, SocketOptionName.IPv6Only, 0);
+```
+
+
+#### 実行結果
+```
+ChristieDaemon, listen: bind to 10001
+ChristieDaemon, listen: bind to 10002
+Accept localhost:55790
+connect@localhost:55790
+
+```
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2021-04-20.md	Wed Apr 21 00:10:03 2021 +0900
@@ -0,0 +1,61 @@
+# 研究目的(研究会に出す方)
+- OSやアプリケーションの信頼性を高めることは重要な課題である。
+
+- 研究室でCbCという言語を開発している。その信頼性を証明したい。
+
+    - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
+
+- プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。
+
+    - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
+
+- これらのことから、Hoare Logicを用いてCbCを検証する。
+
+- cbcはサブルーチンとスープ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。
+
+- 先行研究ではCbCにおけるWhileLoopの検証を行なった。
+
+- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う
+
+# 研究目的(修士の方)(途中)
+- CbCにはあまりよくない部分がある
+    - interfaceとか
+
+- RustをContinuetion styleにしたものを作成し、Agdaで検証する
+
+# やった事
+
+- モデル検査について調べていた
+
+- LLVMについても勉強したかった
+    - 「きつねさんでもわかるLLVM」を読んでいたが、難しくて寝てしまった(つまり僕の理解力はきつねさん以下だった…)
+
+## モデル検査について
+Agdaでモデル検査をする事をkono先生が言っていたので、調べていた
+
+- モデル検査はUnitTestを大量にやる感じの検証手法(ここから調べていた)
+
+- AgdaでNuSMVというものが呼び出せるプラグインを産業技術総合研究所システム検証研究センター作っているみたいだった
+
+- というわけで、nusmvで遊んでいた
+    - 昔(b4くらいの時)kono先生が言っていた`2*x`と`x+x`の検証してみたかったが、上手く動かせなかった。
+
+- 参考
+    - [検証における記述量爆発問題の構造変換による解決](https://www.jst.go.jp/kisoken/crest/report/heisei17/pdf/a18/f01/s005.pdf)
+    - [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 を適応出来たら嬉しい
+- Agdaで Red Black Tree を作成する
+    - 実はもうちょっとでできそうな感じがある。頑張ってみる
+- 研究計画書
+    - なぜかアナウンスがまるでない…
+
+# 余談
+- M1 MacBook Air でAgda on Spacemacs が動くか検証していた
+    - ちゃんと動きました。やったね
\ No newline at end of file