# HG changeset patch
# User autobackup
# Date 1651590603 -32400
# Node ID d3c2798ce6d777901dc6a49c304ffb2faa39e5f7
# Parent  154ee3bc4903322785ce133867481ff5059551da
backup 2022-05-04

diff -r 154ee3bc4903 -r d3c2798ce6d7 user/matac42/note/2022/05/03.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2022/05/03.md	Wed May 04 00:10:03 2022 +0900
@@ -0,0 +1,22 @@
+# 研究目的
+
+## GearsOSにおけるメモリ管理とそれに対応する分散FS
+
+- アプリケーションの信頼性を保証するために，アプリケーションが動作するOSの信頼性を高める必要がある
+- 当研究室では，信頼性の保証を目的としたGearsOSを開発している
+- GearsOSで未実装の機能であるメモリ管理システムを構築、考察しそれに対応する分散FSを考察する
+
+要件
+
+- モデル検査による信頼性の保証
+  - CbCによるノーマルレベル、メタレベルの切り分け
+
+取り入れたい要素
+
+- transaction
+- backup & logging
+- unix like
+
+# 研究会論文
+
+- メモリマネージャーにつなげたい
\ No newline at end of file
diff -r 154ee3bc4903 -r d3c2798ce6d7 user/mizuki/メモ/2022/05/03.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/mizuki/メモ/2022/05/03.md	Wed May 04 00:10:03 2022 +0900
@@ -0,0 +1,37 @@
+## 研究目的
+
+近年のシステムの大規模化・複雑化もあり、ログの設定は多種多様で都度適切な設定をするのは難しい。
+それらの設定を日々用いるメッセージングツールから行うことで管理者の負担が減ると考える。
+
+## やったこと
+研究環境ではdocker-composeで監視システムが動いていたのでpodに変更する。 
+```
+空のpod生成  
+podman pod create -p 9090:9090 -p 3000:3000 -p 9113:9113 -p 9100:9100 -p 9312:9312 -p 9093:9093 -p 3100:3100 -n monitoring-system
+
+podにコンテナを追加  
+ podman run -dt --pod monitoring-system -u 0 -v ./var-lib-grafana:/var/lib/grafana -v ./grafana/grafana.ini:/etc/grafana/grafana.ini docker.io/grafana/grafana
+ podman run -dt --pod monitoring-system -v ./loki/local-config.yaml:/etc/loki/local-config.yaml -v ./loki/config:/loki/rules docker.io/grafana/loki
+ podman run -dt --pod monitoring-system -v ./prometheus:/etc/prometheus -v ./prometheus/alert.rules:/etc/prometheus/alert.rules docker.io/prom/prometheus
+ podman run -dt --pod monitoring-system -v ./ssh/ssh_exporter.yaml:/ssh_exporter.yaml:ro -v /home/skm-user/.ssh:/.ssh:ro docker.io/treydock/ssh_exporter
+ podman run -dt --pod monitoring-system -v ./alertmanager:/etc/prometheus docker.io/prom/alertmanager
+ podman run -dt --pod monitoring-system -v /proc:/host/proc quay.io/prometheus/node-exporter
+ podman run -dt --pod monitoring-system -v ./nginx/nginx-prometheus-exporter.service:/lib/systemd/system/nginx-prometheus-exporter.service docker.io/nginx/nginx-prometheus-exporter```
+ 
+追加したpodを元にk8sのyamlを生成  
+podman generate kube monitoring-system > monitoring-system.yaml
+
+生成したyamlを元にpodを生成  
+podman play kube monitoring-system.yaml
+
+上記で動作確認したところ全部が正常に動作しているわけではなかった。  
+多分docker-composeはコンテナ名を使用してコンテナ間の通信ができるがpodではそれができないから？  
+マウントしている設定ファイルを書き換える必要あり。  
+それ以外にも原因あると思う。  
+  
+```
+
+podmanはCLIからではネットワークが作成できない
+なので、podman-networkを用いる
+
+OS研究会の提出する論文を書き始めました。
\ No newline at end of file
diff -r 154ee3bc4903 -r d3c2798ce6d7 user/soto/log/2022-05-03.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2022-05-03.md	Wed May 04 00:10:03 2022 +0900
@@ -0,0 +1,55 @@
+# SIGOSに出す研究目的
+
+思い思いにプログラムを書くと、冗長なコードができてしまい、
+実行時間も遅い場合がある。
+
+この場合にコードに対してアルゴリズムを適応すると実行が最適化され
+実行時間が減り、かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。
+つまり、一般的に良いコードが作成できる。
+
+しかし、世の中にはすでに大量のアルゴリズムが存在するため、
+これを一人のプログラマーが全て覚え、適応できる場面を思いつくというのは不可能に近い。
+その道に詳しい人が複数人いる場面というのも稀だと考えられる。
+
+そのため、人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。
+
+この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。
+一般的なプログラミング言語では、関数の遷移が自由であることから、関数遷移などで発生した
+暗黙の環境が存在するためである。
+
+この問題を解決するため、Gears Agda を用いる。
+
+Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと
+通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。
+この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、
+スタックしていた変数をもとに戻す流れとなる。
+CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。
+更に遷移後にメインルーチンに戻ることもない。
+つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
+これにより限定的な実行条件を作成でき、検証がしやすくなる。
+
+現在、アルゴリズムの適応可否は以下の方法を考えている。
+
+あらかじめ、アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく
+
+書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき、
+満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている。
+
+この際、実装が仕様を満たしているか検証する手法には、定理証明やモデル検査などが挙げられる。
+
+アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い、アルゴリズムの仕様がコードに適応できるか検証するのが
+妥当だと考えている
+思い思いに書いたコードに対して定理証明を行うのはコストが高く、適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。
+
+本論文では Gears Agda でのモデル検査の先駆けとして Dining philosophers problem (DPP) のモデル検査を行う。
+
+# 進捗
+- DPPを実装している
+    - Model Checkingの実装から永遠に進んでいない
+    - kono先生に言われた修正も途中まではできた(下記がまだ)
+        - DPPの通常実行
+        - stubを使用したCodeの記述
+        - 上にもかいたdead lockの検出
+    - 実行の網羅はできた(やったね)
+
+- 論文を1Pだけ書いた(最初の目的の部分だけ)
\ No newline at end of file