Mercurial > hg > Document > Growi

--- a/user/Okud/メモ/2021/01/24.md	Tue Jan 26 00:10:03 2021 +0900
+++ b/user/Okud/メモ/2021/01/24.md	Wed Jan 27 00:10:04 2021 +0900
@@ -32,6 +32,9 @@
         - RPI_EFI.FDではUEFIが起動しない
             - FDファイルを自分で作る必要がある
         - qemuのオプションに何があるかまだわかってない
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2021/01/26.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,104 @@
+# 研究目的
+- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
+    - しかしOSの機能をテストですべて検証するのは不可能である。
+- 定理証明やモデル検査を利用して、テストに頼らずに保証したい
+    - 証明しやすい形、かつ実際に動くソースコードが必要
+    - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
+- プログラムは二つの計算に分離される
+    - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
+    - その計算に必要なメタな計算(メタレベル)
+- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
+- そのためにはメタレベルの計算を柔軟に扱うAPIや, メタレベルを保証しつつCbCを拡張した実装方法が必要
+- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。
+
+# 今週
+- 修論本体書き始め
+- 論文審査は2月の第1週くらいっぽい
+    - 山田先生の反応待ち
+- DPPの実装メインで今は作業中
+    - 自分の修論にいれていい内容なのかは微妙な気がする
+- 終わったらGenericsとlambdaあたりいれたい
+
+
+# meta.pm
+
+変更したい`.cbc`があるディレクトリに`meta.pm`を置く
+
+
+```perl
+package meta;
+use strict;
+use warnings;
+
+sub replaceMeta {
+  return (
+    [qr/PhilsImpl/ => \&generateMcMeta],
+    #[qr/.+/         => \&all],
+  );
+}
+
+#my ($currentCodeGearName, $context, $next) = @_;
+
+sub generateMcMeta {
+  my ($context, $next) = @_;
+  return "goto mcMeta($context, $next);";
+}
+
+1;
+```
+
+
+重要なとこは`replaceMeta`
+
+
+```perl
+sub replaceMeta {
+  return (
+    [qr/PhilsImpl/ => \&generateMcMeta],
+    #[qr/.+/         => \&all],
+  );
+}
+```
+
+- 多次元リストを返す
+- 各要素は先頭が正規表現リテラルである必要がある
+    - 変更したいCodeGearの名前を指定する
+    - マッチすると2つめの値で指定したサブルーチンが実行される
+- サブルーチンはcontextの名前とnextが渡る
+    - 他に渡したい場合は`generate_stub.pl`を変更すればOK
+- デフォルトは`goto meta`が生成される
+- `extern __code mcMeta`みたいなのは手で書く必要がある
+    - 単純にサボっているだけ...
+
+
+- こんな感じで初期化している
+    - `Module::Load`を使うと動的ロード可能(`@INC` + requireでもできるが...)
+
+```perl
+sub generateDefaultgotoMeta {
+  my (undef, $context, $next) = @_;
+  return "goto meta($context, $next);";
+}
+
+sub createGotoMetaFunction {
+  my $filename = shift;
+  my $project_dir_name = dirname $filename;
+  my $metapm = "$FindBin::Bin/$project_dir_name/meta.pm";
+  unless (-f $metapm) {
+    #default case
+    return \&generateDefaultgotoMeta;
+  }
+
+  load $metapm;
+  print "[info] load $metapm\n";
+  my @replaceMeta = meta->replaceMeta();
+  return sub {
+    my ($currentCodeGearName, $context, $next) = @_;
+     my $generator = shift @{[ map { $_->[1] } grep { $currentCodeGearName =~ $_->[0]  } @replaceMeta ] };
+     unless ($generator) {
+       return generateDefaultgotoMeta(undef, $context, $next);
+     }
+     return $generator->($context, $next);
+  };
+}
+```
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/aosskaito/メモ/2021/01/26.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,14 @@
+#
+## 研究目的
+-
+
+## 興味あること
+- 言語系とか
+- フレームワーク関連
+- レトロゲーム
+- これがやりたい！ってのがなかなか見つからない
+
+
+## 調べること
+-
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/masato/メモ/2021/01/19.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,18 @@
+#
+## 研究目的
+
+
+## 興味あること
+### サウンド
+環境推定からの音響再現
+
+空間の広さ、材質からリバーブのパラメータを変える
+
+音の発生方向により特定周波数の減衰を行う
+
+NierAutomataあたりでまとめられていた
+
+#### リバーブ
+畳み込み,周波数領域での乗算
+
+アルゴリズム　FDN,Gverb
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2021/01/26.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,22 @@
+# 興味があること
+* CbCにたどり着くまでの道のり
+
+# 調べること
+* 赤黒木ってなんだっけ
+    * アルゴリズムとデータ構造にあった気が
+* モデル検査
+    * モデルとは
+    * first order logic
+    * あらゆる変数の可能な値を調べていく
+    * あらゆる可能な実行を調べていく
+    * agdaの場合は証明があるかどうか?
+    * Java Pathfinderがあやふや
+    * プログラミングの中でモデル検査や定理証明ができたら良いなぁという感じらしい．
+# メモ
+webpageとmercurialをfireflyからdalmoreに移行する
+droneとcircleci
+amaneとdalmoreにCbCをビルドできるsingularityがあるよ(mk)
+* `singularity shell /ie-ryukyu/singularity/cbc_gcc/cbc_gcc.sif`
+ついにmacでもsingularityが！（beta版, まだbuildはできない shellやrunだけ）
+* https://sylabs.io/singularity-desktop-macos/
+なんかvimrcエラー吐くからから直す
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/2021/01/19.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,27 @@
+# Gears OS
+## 研究目的
+- なんとなくOSやりたい
+- ファイルシステム
+- x.v6のファイルシステムの書き換え
+
+
+## 調べること
+- ceph
+- x.v6のファイルシステム
+- docker
+- vhat
+- aufs
+- singularity
+- コンテナの強調して動くファイルシステム
+- GearsOSのファイルシステムもそうであるべき
+- メタコンピューテーション
+- java reflection
+- 圏論のモナド
+- 単一モナド
+- x.v6のファイルシステムのcbcで書き直す
+- cephは分散ファイルシステム
+- クラスター化されたファイルシステム
+- christie
+- jungle
+- 上記2つを
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/2021/01/26.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,17 @@
+# Gears OS
+## 研究目的
+- なんとなくOSやりたい
+- ファイルシステム
+- x.v6のファイルシステムの書き換え
+
+## 今週やったこと
+- 面接をたくさんやった(3社)
+- コンパイラとインターネットアーキテクチャの課題
+- シス管のタスクをちょこっとやった
+
+## 来週やること
+- 2/4 GTEC
+- 先週のゼミで言われた調べ物
+- 大学院科目早期履修とGEの書類提出
+- 早めに研究を始めたい
+- 最終面接。。。
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/__template.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,1 @@
+redirect /trash/user/pine/note/__template
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/note/__template/_template.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,1 @@
+redirect /trash/user/pine/note/__template/_template
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/riono210/seminar/202101/0126.md	Wed Jan 27 00:10:04 2021 +0900
@@ -0,0 +1,121 @@
+## 01/26
+
+## 研究目的
+* ゲームの通信方式にはクライアントサーバ方式とp2p方式がある
+* データの安全性やチート対策などでクライアントサーバ方式が主流
+* サーバに接続してマルチプレイなどのデータ同期を実現させているため、低速
+* 高速かつ安全に通信を行たい
+    * 並列分散フレームワークChristieがある
+    * Christieを利用してp2pで通信を行う
+* ゲーム開発で主に使用されているUnityに対応するためにChristieをC#へ書き換えを行う
+
+## 今週の進捗
+* ChristieのHelloWorldを動かすために必要なコードを書き切った
+    * 案の定動かない
+    * どうもFinishCodeGearが実行されていない
+        * Task周りの問題?
+* OSのTA
+    * いまだにFileWirteとかを聞かれる
+    * 今年もヤバそう...
+    * 学サポに来てる人はまだマシそう...
+* 大辛チャレンジ
+    * かなり辛い... ヤバイ...
+
+
+## Christie
+```
+/usr/local/share/dotnet/dotnet /Users/e165729/konoLab/Christie_net/bin/Debug/netcoreapp3.1/Christie_net.dll
+ChristieDaemon, listen: bind to [::1]:10000
+HelloWorldCodeGear Take =>
+HelloWorldCodeGear Take =>
+
+Process finished with exit code 0.
+```
+エラーも出ずに終了してしまう。
+
+
+```c
+public static void Main(string[] args) {
+  CodeGearManager cgm = CreateCgm(10000);
+  cgm.Setup(new HelloWorldCodeGear());
+  cgm.Setup(new FinishHelloWorld());
+  cgm.GetLocalDGM().Put("helloWorld", "hello");
+  cgm.GetLocalDGM().Put("helloWorld", "world");
+    }
+```
+
+```c
+public class HelloWorldCodeGear : CodeGear {
+    [Take] private string helloWorld;
+
+    public override void Run(CodeGearManager cgm) {
+        Console.WriteLine("HelloWorldCodeGear Take => " +helloWorld);
+        cgm.Setup(new HelloWorldCodeGear());
+        cgm.GetLocalDGM().Put(helloWorld, helloWorld);
+    }
+}
+```
+
+```c
+public class FinishHelloWorld : CodeGear {
+    [Take] private string hello;
+    [Take] private string world;
+
+    public override void Run(CodeGearManager cgm) {
+        Console.WriteLine("fin:" + hello + " " + world);
+        cgm.GetLocalDGM().Finish();
+    }
+}
+```
+
+### 優先度つきTreadPoolについて
+Taskは内部的にThreadPoolを使っている
+Task生成時にTaskSchedulerを指定できる
+→TaskSchedulerを継承して自作する
+→内部のwaitQueueの順番を操作することが可能
+→java版と同じように優先度がつけれそう
+
+
+### リフレクションで死んでしまった
+```c#
+foreach (var field in this.GetType().GetFields(BindingFlags.Public | BindingFlags.NonPublic |
+                                                       BindingFlags.DeclaredOnly | BindingFlags.Instance)) {
+            if (Attribute.IsDefined(field, typeof(Take))) {
+                SetCommand(CommandType.TAKE, "local", field.Name, new DataGear<object>(field.FieldType));
+            } else if (Attribute.IsDefined(field, typeof(Peek))) {
+                SetCommand(CommandType.PEEK, "local", field.Name, new DataGear<object>(field.FieldType));
+            } else if (Attribute.IsDefined(field, typeof(TakeFrom))) {
+                TakeFrom attri = (TakeFrom) field.GetCustomAttribute(typeof(TakeFrom));
+                SetCommand(CommandType.TAKE, attri.name, field.Name, new DataGear<object>(field.FieldType));
+            } else if (Attribute.IsDefined(field, typeof(PeekFrom))) {
+                PeekFrom attri = (PeekFrom) field.GetCustomAttribute(typeof(PeekFrom));
+                SetCommand(CommandType.PEEK, attri.name, field.Name, new DataGear<object>(field.FieldType));
+            }
+        }
+```
+
+`DataGear<object>(field.GetType())`だとtypeがRuntimeTypeになってしまった。
+fieldのメンバにFieldTypeがあったのでそれを使ったら直った。
+
+---
+### IPAddressが0だと死ぬ
+
+
+```c
+// listen on any address ipv4/ipv6
+            IPHostEntry host = Dns.GetHostEntry("::");
+            IPAddress ipAddress = host.AddressList[0];
+            IPEndPoint localEndPoint = new IPEndPoint(ipAddress, localPort);
+
+            Socket socket = new Socket(ipAddress.AddressFamily, SocketType.Stream, ProtocolType.Tcp);
+            socket.SetSocketOption(SocketOptionLevel.Socket, SocketOptionName.ReuseAddress, true);
+            Console.WriteLine("ChristieDaemon, listen: bind to " + localEndPoint);
+            socket.Bind(localEndPoint);
+            socket.Listen((int)SocketOptionName.MaxConnections);
+
+```
+
+`IPHostEntry host = Dns.GetHostEntry("::");`だとダメ
+`IPHostEntry host = Dns.GetHostEntry("::1");`で一応動いている。
+
+
--- a/user/soto/log/untitled.md	Tue Jan 26 00:10:03 2021 +0900
+++ b/user/soto/log/untitled.md	Wed Jan 27 00:10:04 2021 +0900
@@ -1,1 +1,31 @@
-redirect /user/soto/log/2021-01-19
\ No newline at end of file
+# 研究目的
+
+- OSやアプリケーションの信頼性を高めることは重要な課題である。
+
+- 研究室でCbCという言語を開発している。その信頼性を証明したい。
+    - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
+
+- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。
+
+- プログラムの検証手法のひとつに、Hoare Logic がある。
+    - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。
+
+    - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。
+
+    - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
+
+
+- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。
+
+- これらのことから、Hoare Logicを用いてCbCを検証する。
+
+
+- 先行研究ではCbCにおけるWhileLoopの検証を行なった。
+
+- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う
+
+# 今週やった事
+- スライドの作成
+
+## 余談
+-　明日が入試当日