2021/01/05

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を継続にいれる
1
2
3
4
5
6
7
8
#interface "Stack.h"
#interface "StackTest.h"

__code gmain(){
    Stack* stack = createSingleLinkedStack(context);
    StackTest* stackTest = createStackTestImpl3(context);
    goto stackTest->insertTest1(stack, shutdown);
}

# 変換後

  • 基本的に今まで使ってたやつに変換される
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
#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をしている箇所で引数検査を行う
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
[
    [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(...)
  • そもそもそんなメソッドが無いケースも判定
1
2
[ERROR] not found phils0 definition at     par goto phils0->think(fork0, __exit);
 in c/examples/DPP/main.c
Licensed under CC BY-NC-SA 4.0
comments powered by Disqus
Built with Hugo
Theme Stack designed by Jimmy