changeset 17:4d2f07e4f23e

backup 2021-01-06
author autobackup
date Wed, 06 Jan 2021 00:10:03 +0900
parents a6fe06ec0cf9
children 46800d30a182
files user/anatofuz/note/2021/01/05.md user/jogo/memo/2021/01/05.md
diffstat 2 files changed, 227 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2021/01/05.md	Wed Jan 06 00:10:03 2021 +0900
@@ -0,0 +1,199 @@
+# 2021/01/05
+
+# 研究目的
+- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
+    - しかしOSの機能をテストですべて検証するのは不可能である。
+- 定理証明やモデル検査を利用して、テストに頼らずに保証したい
+    - 証明しやすい形、かつ実際に動くソースコードが必要
+    - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
+- プログラムは二つの計算に分離される
+    - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
+    - その計算に必要なメタな計算(メタレベル)
+- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
+- そのためにはメタレベルの計算を柔軟に扱うAPIや実装方法が必要
+- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。
+
+# 最近
+- あけましておめでとうございます
+- ThinkPadにLinuxデスクトップインストールバトル
+    - wsl2も使ってみた
+    - manjaroをいれたかったけど今はubuntu
+    - そこそこ安定
+- Gearsでmain.cを生成するスクリプトを組んだ
+- シス管関係
+- プログラミング(Java)の学サポ
+- hg-browseの改修
+    - linux対応
+        - 自分が使いたい
+    - コアモジュール対応
+
+
+
+# hg-browse
+
+- hg webのページをコマンド一発で起動するPerlスクリプト
+  - hg config読み込んで, URLを組み立ててopenする
+- linuxだと`xdg-open`
+
+# Gmain
+- Gearsのメイン関数難しい問題がある
+    - いろいろおまじないが多い
+- この前`generate_stub.pl`の処理を多少変更した
+    - 以前
+        - cbcファイルを読み込んで処理(`getDataGear`)
+        - もう一度読みながら`*.c`を生成(`generateDataGear`)
+    - 現在
+        - cbcファイルを読み込んで処理(`getDataGear`)
+        - すでに配列に保存されているcbcを読みながら`*.c`を生成(`generateDataGear`)
+- `generateDataGear`の前でPerlの処理の中だけでcbcを書き換えることが出来る
+- ということで`.cbc` -> `.cbc(Perlの中で生成)` -> `.c` に置き換えるフローを構築してみた
+
+## gmain
+
+- 終わりたいときは`shutdown`を継続にいれる
+
+```c
+#interface "Stack.h"
+#interface "StackTest.h"
+
+__code gmain(){
+    Stack* stack = createSingleLinkedStack(context);
+    StackTest* stackTest = createStackTestImpl3(context);
+    goto stackTest->insertTest1(stack, shutdown);
+}
+```
+
+## 変換後
+
+- 基本的に今まで使ってたやつに変換される
+
+```c
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+#include "../../../context.h"
+
+int cpu_num = 1;
+int length = 102400;
+int split = 8;
+int* array_ptr;
+int gpu_num = 0;
+int CPU_ANY = -1;
+int CPU_CUDA = -1;
+
+__code initDataGears(struct Context *context,struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    // loopCounter->tree = createRedBlackTree(context);
+    loopCounter->i = 0;
+    taskManager->taskManager = (union Data*)createTaskManagerImpl(context, cpu_num, gpu_num, 0);
+    goto meta(context, C_prevTask);
+}
+
+__code initDataGears_stub(struct Context* context) {
+        LoopCounter* loopCounter = Gearef(context, LoopCounter);
+        TaskManager* taskManager = Gearef(context, TaskManager);
+        goto initDataGears(context, loopCounter, taskManager);
+}
+
+__code prevTask(struct Context *context,struct LoopCounter* loopCounter) {
+    printf("cpus:\t\t%d\n", cpu_num);
+    printf("gpus:\t\t%d\n", gpu_num);
+    printf("length:\t\t%d\n", length);
+    printf("length/task:\t%d\n", length/split);
+    /* puts("queue"); */
+    /* print_queue(context->data[ActiveQueue]->queue.first); */
+    /* puts("tree"); */
+    /* print_tree(context->data[Tree]->tree.root); */
+    /* puts("result"); */
+    goto meta(context, C_createTask);
+}
+
+
+__code prevTask_stub(struct Context* context) {
+        LoopCounter* loopCounter = Gearef(context, LoopCounter);
+        goto prevTask(context, loopCounter);
+}
+
+__code createTask(struct Context *context,struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    Stack* stack = createSingleLinkedStack(context);
+    StackTest* stackTest = createStackTestImpl3(context);
+    Gearef(context, StackTest)->stackTest = (union Data*) stackTest;
+    Gearef(context, StackTest)->stack = stack;
+    Gearef(context, StackTest)->next = C_shutdown;
+    goto meta(context, stackTest->insertTest1);
+}
+
+__code createTask_stub(struct Context* context) {
+        LoopCounter* loopCounter = Gearef(context, LoopCounter);
+        TaskManager* taskManager = Gearef(context, TaskManager);
+        goto createTask(context, loopCounter, taskManager);
+}
+
+__code shutdown(struct Context *context,struct TaskManager* taskManager) {
+    Gearef(context, TaskManager)->taskManager = (union Data*) taskManager;
+    Gearef(context, TaskManager)->next = C_exit_code;
+    goto meta(context, taskManager->shutdown);
+}
+
+__code shutdown_stub(struct Context* context) {
+    goto shutdown(context, &Gearef(context, TaskManager)->taskManager->TaskManager);
+}
+
+
+
+void init(int argc, char** argv) {
+    for (int i = 1; argv[i]; ++i) {
+        if (strcmp(argv[i], "-cpu") == 0)
+            cpu_num = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-l") == 0)
+            length = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-s") == 0)
+            split = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-cuda") == 0) {
+            gpu_num = 1;
+            CPU_CUDA = 0;
+        }
+    }
+}
+
+int main(int argc, char** argv) {
+    init(argc, argv);
+    struct Context* main_context = NEW(struct Context);
+    initContext(main_context);
+    main_context->next = C_initDataGears;
+    goto start_code(main_context);
+}
+```
+
+# コンパイル時チェック機能
+
+- Interfaceの引数があってないのがありがち
+    - `generate_stub.pl`で生成された`.c`と`.cbc`をにらめっこしないといけない
+    - 気づくまで難しい, 気づかないケースがある(今までの実装)
+- `generate_stub.pl`の中でinterface gotoをしている箇所で引数検査を行う
+
+```
+[
+    [0] {
+        argc   1,
+        args   "Impl* phils, __code next(...)",
+        name   "thinking"
+    }
+]
+[
+    [0] "fork0",
+    [1] " __exit"
+]
+1
+[EROR] invalid arg     par goto phils0->thinking(fork0, __exit);
+  you shoud impl Impl* phils, __code next(...)
+```
+
+- そもそもそんなメソッドが無いケースも判定
+
+```c
+[ERROR] not found phils0 definition at     par goto phils0->think(fork0, __exit);
+ in c/examples/DPP/main.c
+```
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/jogo/memo/2021/01/05.md	Wed Jan 06 00:10:03 2021 +0900
@@ -0,0 +1,28 @@
+# 研究目的
+
+多段 ssh 接続を管理する sshr の改良
+
+## 研究内容
+
+目的のサーバにアクセスするために外部からサーバへのアクセスへは踏み台サーバからのアクセスが必要である.踏み台サーバでは外部から第三者に乗っ取られることや不特定多数の攻撃の中継地点を防止するためのものである.しかし,利用している踏み台サーバが停止すると学内での復旧作業が必要になってしまうそこで,新規踏み台サーバとしてsshrを提案する.sshrは鶴田博文氏が作成したものである.sshrはシステム管理者が組み込み可能なフック関数を用いてシステム変化に追従できるsshプロキシサーバである.本稿ではsshrを改良し弊学へ利用できるように実装をした.
+
+# sshrのを改良した
+- openssh7.8以上の秘密鍵で認証できるように対応した.
+- 本家のx/ssh/cryptoで議論されてたissueをコピペして直せた
+- テストを追加すれば本家にPR送っていいかもしない
+
+# フリーマインドを書いた
+- https://gitlab.ie.u-ryukyu.ac.jp/k198576/master-paper
+- 欲望のように書いてこれであってるのか..?と思いながら書いてました
+
+
+# シス管
+- latexのDockerfileを探していた
+- 見つけたが画像を表示してくれないのでlatexliveの全てのパッケージ込みのものをビルドしている最中
+- 試して画像の出力などもできたらamaneのコンテナレジストリにpushする
+- buildしてたらpdfを吐き出せてないので失敗してそう.
+
+# 次の家が決まった
+- 書類を書いています
+- 早く終わらせたい
+