# HG changeset patch
# User autobackup
# Date 1653405003 -32400
# Node ID dc7f6570e57265e23cd9b13dfbd65d5500dd96e5
# Parent  fe83f758e452fe0f42188df40f674204a4ce1312
backup 2022-05-25

diff -r fe83f758e452 -r dc7f6570e572 user/matac42/note/2022/05/24.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2022/05/24.md	Wed May 25 00:10:03 2022 +0900
@@ -0,0 +1,24 @@
+# 研究目的
+
+## GearsOSにおけるメモリ管理とそれに対応する分散FS
+
+- アプリケーションの信頼性を保証するために，アプリケーションが動作するOSの信頼性を高める必要がある
+- 当研究室では，信頼性の保証を目的としたGearsOSを開発している
+- GearsOSで未実装の機能であるメモリ管理システムを構築、考察しそれに対応する分散FSを考察する
+
+要件
+
+- モデル検査による信頼性の保証
+  - CbCによるノーマルレベル、メタレベルの切り分け
+
+取り入れたい要素
+
+- transaction
+- backup & logging
+- unix like
+
+# 研究会
+
+## 発表スライド
+
+- ほとんど卒検と変わらないが，メモリの話を入れた．
\ No newline at end of file
diff -r fe83f758e452 -r dc7f6570e572 user/mizuki/メモ/2022/05/24.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/mizuki/メモ/2022/05/24.md	Wed May 25 00:10:03 2022 +0900
@@ -0,0 +1,18 @@
+## 研究目的
+
+・システムの安定運用には物理機器の経年劣化によるトラブルやサービスのバージョンアップによるシステムトラブル, 外部からの攻撃などによるインシデントなどに対応するためにサービスのログが重要である. 
+
+・システムやユーザーの挙動の必要なものを選択し,ログに記述する.インシデントがおきている場合はそれを検出し,通知したい.   
+
+・ログを調べることによりインシデントの場所を特定し, 修復を行う.  
+
+・複数のサーバーやVM, コンテナに分散しているログを集約する必要がある.
+
+・大量のログ設定を手動で管理することは現実的ではない. 
+
+・そこでログ管理システムだけでなくログ管理システムの設定方法自体を改良していくことが必要である.
+
+## 進捗
+・スライドを書きました  
+・podを使用してのサービス起動がまだ出来ない  
+起動時のコマンドが読み込めてない
diff -r fe83f758e452 -r dc7f6570e572 user/soto/log/2022-05-24.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2022-05-24.md	Wed May 25 00:10:03 2022 +0900
@@ -0,0 +1,48 @@
+# 研究目的
+# SIGOSに出す研究目的
+
+- 思い思いにプログラムを書くと、冗長なコードができてしまい、
+  実行時間も遅い場合がある。
+
+- この場合にコードに対してアルゴリズムを適応すると実行が最適化され
+  実行時間が減り、かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。
+  つまり、一般的に良いコードが作成できる。
+
+- しかし、世の中にはすでに大量のアルゴリズムが存在するため、
+  これを一人のプログラマーが全て覚え、適応できる場面を思いつくというのは不可能に近い。
+  その道に詳しい人が複数人いる場面というのも稀だと考えられる。
+
+- そのため、人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。
+
+- この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。
+  一般的なプログラミング言語では、関数の遷移が自由であることから、関数遷移などで発生した
+  暗黙の環境が存在するためである。
+
+- このアルゴリズム適応前後の処理の恒等性を検証するため、Gears Agda を用いる。
+
+  - Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと
+  - 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。
+    この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、スタックしていた変数をもとに戻す流れとなる。
+  - CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。
+  - つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
+  - これにより限定的な実行条件を作成でき、検証がしやすくなる。
+
+- 現在、アルゴリズムの適応可否は以下の方法を考えている。
+
+  - あらかじめ、アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく
+
+  - 書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき、
+    満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている。
+
+- この際、実装が仕様を満たしているか検証する手法には、定理証明やモデル検査などが挙げられる。
+
+  - アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い、アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている
+  - 思い思いに書いたコードに対して定理証明を行うのはコストが高く、適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。
+
+- アルゴリズムの入れ替え可否をモデル検査で判定し、入れ替えたあとに適応前後で同じ処理をしていることを
+  定理証明で検証できるととても嬉しい
+
+
+# 進捗
+- Gears Agdaの方でDPPのモデル検査でデッドロックを検知できるようになった
+- スライドを書いていた