# 研究目的

OSの信頼性を保証する必要がある
信頼性の保証にはモデル検査や定理証明を使用したい
- 継続ベースの状態遷移系で再実装することで表現しやすくしたい
既存のunixであるxv6をCbCで書き換えて、検証を行いやすくしたい
- kernel/user両方をCbCで実装する

# 最近

シス管関連
- LDAPの構築
  - とりあえず元気にubuntu上で動いているのでしばらく安泰
- radius
- その他ansible
  - ansibleの書き方だいぶわかってきた気がする
Gears
- Interfaceの実装を満たしていないとエラーを出す
- コンストラクタの自動生成
- Interfaceの実装の名前空間の実装

# Gears Interface

満たしていないmethodが生えているとコンパイルタイムでエラーを出す
- Interfaceの実装のファイルの場合、実装したメソッドを数え上げている
- ルール的には第一引数にImplが来ている (満たすべきCodeGear)だけ回収

1
2
3
4
5
6
7


$ make pop_and_push
[  7%] Generating c/examples/pop_and_push/StackTestImpl3.c
[ERROR] Not define insertTest4 at examples/pop_and_push/StackTestImpl3.cbc
make[3]: *** [c/examples/pop_and_push/StackTestImpl3.c] Error 255
make[2]: *** [CMakeFiles/pop_and_push.dir/all] Error 2
make[1]: *** [CMakeFiles/pop_and_push.dir/rule] Error 2
make: *** [pop_and_push] Error 2

generate_stubの初回のcbcの読み込み時に数え上げと判定を行う
- 実装するべきCodeGearをパターンマッチする愚直な実装

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


    if ($implInterfaceInfo->{isImpl} && $filename =~ /\.cbc\z/) {
      for my $shouldImplCode (map { $_->{name} } grep { $_->{args} =~ /Impl/ } @{$implInterfaceInfo->{parsedInterfaceInfo}->{codes}}) {
        my $isDefine = $shouldImplCode;
        for my $implCode (keys %{$codeGearInfo}) {
          if ($implCode =~  /$shouldImplCode/) {
            $isDefine = 1;
            next;
          }
        }

        if ($isDefine ne 1) {
          die "[ERROR] Not define $isDefine at $filename\n";
        }
      }
    }

# 名前空間の実装

InterfaceのImplの際にpopSingleLinkedStackなどの様な__code {interfaceMethod}{ImplType}の命名規則が敷かれている
- 他の言語(eg, java, golang, Rust, Haskell)等では実装名が関数名に付随することはあまりない
  - このあたりはコンパイラ側が吸収しているはず
- 現状は手で書く or trans_impl.plでInterfaceの名前と実装の方名から.cbcを自動生成するアプローチ
  - 実装はInteraceのCodeGearの名前で書いて、命名規則の変換をgenerate_stubのタイミングで行いたい
新しい記法#implを導入した

# 基本ルール

#impl "Stack.h"
- Stack.hを実装している場合に記述する
- この場合は自分の.cbcのファイル名と実装の型名が一致している前提
  - SingleLinkedStack.cbcの場合　-> SingleLinkedStack.hが存在しないとだめ
#impl "StackTest.h" for "StackTestImpl3.h"
- Inteerface for 型名の順で書く
- この場合は実装する.cbcとヘッダファイルの名前が異なっても大丈夫

# 実際に書く

# ヘッダ

1
2
3
4
5
6
7
8
9


typedef struct StackTest <Type, Impl> {
  __code insertTest1(Impl* stackTest, struct Stack* stack, __code next(...));
  __code insertTest2(Impl* stackTest, struct Stack* stack, __code next(...));
  __code insertTest3(Impl* stackTest, struct Stack* stack, __code next(union Data* data, union Data* data1, ...));
  __code insertTest4(Impl* stackTest, struct Stack* stack, __code next(...));
  __code pop2Test(Impl* stackTest, struct Stack* stack, __code next(...));
  __code pop2Test1(Impl* stackTest, union Data* data, union Data* data1, struct Stack* stack, __code next(...));
  __code next(...);
} StackTest;

# 実装

継続で渡すinsertTest1などは変換される

 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


#include "../../../context.h"
#interface "StackTest.h"
#interface "StackTest2.h"
#interface "Stack.h"
#include <stdio.h>

#include "String.h"

#impl "StackTest.h" for "StackTestImpl3.h"


__code insertTest1(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    String* str = NEW(String);
    str->size = 99;
    goto stack->push((union Data*)str, insertTest2);
}

__code insertTest2(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    String* str = NEW(String);
    str->size = 100;
    goto stack->push((union Data*)str, pop2Test);
}


__code pop2Test(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    goto stack->pop2(pop2Test1);
}

__code pop2Test3(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(union Data* data, union Data* data1, ...)) {
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    data = (union Data*)str;
    data1 = (union Data*)str1;

    goto pop2Test1(stackTest, data, data1);
}


__code pop2Test1(struct StackTestImpl3* stackTest, union Data* data, union Data* data1, struct Stack* stack, __code next(...)) {
    String* str = (String*)data;
    String* str2 = (String*)data1;

    printf("%d\n", str->size);
    printf("%d\n", str2->size);
    goto next(...);
}

# 変換後

  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
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153


#include "../../../context.h"
#include <stdio.h>

#include "/Users/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/examples/pop_and_push/String.h"

StackTest* createStackTestImpl3(struct Context* context) {
    struct StackTest* stackTest  = &ALLOCATE(context, StackTest)->StackTest;
    struct StackTestImpl3* StackTestImpl3 = &ALLOCATE(context, StackTestImpl3)->StackTestImpl3;
    stackTest->stackTest = (union Data*)StackTestImpl3;
    stackTest->stack = NULL;
    stackTest->data = NULL;
    stackTest->data1 = NULL;
    stackTest->insertTest1 = C_insertTest1StackTestImpl3;
    stackTest->insertTest2 = C_insertTest2StackTestImpl3;
    stackTest->insertTest3 = C_insertTest3StackTestImpl3;
    stackTest->insertTest4 = C_insertTest4StackTestImpl3;
    stackTest->pop2Test = C_pop2TestStackTestImpl3;
    stackTest->pop2Test1 = C_pop2Test1StackTestImpl3;
    return stackTest;
}


__code insertTest1StackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    String* str = NEW(String);
    str->size = 99;
    Gearef(context, Stack)->stack = (union Data*) stack;
    Gearef(context, Stack)->data = (union Data*)str;
    Gearef(context, Stack)->next = C_insertTest2StackTestImpl3;
    goto meta(context, stack->push);
}

__code insertTest1StackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto insertTest1StackTestImpl3(context, stackTest, stack, next);
}

__code insertTest2StackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    String* str = NEW(String);
    str->size = 100;
    Gearef(context, Stack)->stack = (union Data*) stack;
    Gearef(context, Stack)->data = (union Data*)str;
    Gearef(context, Stack)->next = C_pop2TestStackTestImpl3;
    goto meta(context, stack->push);
}


__code insertTest2StackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto insertTest2StackTestImpl3(context, stackTest, stack, next);
}

__code pop2TestStackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    Gearef(context, Stack)->stack = (union Data*) stack;
    Gearef(context, Stack)->next = C_pop2Test1StackTestImpl3_1;
    goto meta(context, stack->pop2);
}

__code pop2TestStackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto pop2TestStackTestImpl3(context, stackTest, stack, next);
}

__code pop2Test3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next,union Data **O_data,union Data **O_data1) {
	Data* data  __attribute__((unused))  = *O_data;
	Data* data1  __attribute__((unused))  = *O_data1;
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    data = (union Data*)str;
    data1 = (union Data*)str1;

    goto meta(context, C_pop2Test1StackTestImpl3);
}


__code pop2Test3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	Data** O_data = &Gearef(context, StackTest)->data;
	Data** O_data1 = &Gearef(context, StackTest)->data1;
	goto pop2Test3(context, stackTest, stack, next, O_data, O_data1);
}

__code pop2Test1StackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, union Data* data, union Data* data1, struct Stack* stack, enum Code next) {
    String* str = (String*)data;
    String* str2 = (String*)data1;

    printf("%d\n", str->size);
    printf("%d\n", str2->size);
    goto meta(context, next);
}


__code pop2Test1StackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Data* data = Gearef(context, StackTest)->data;
	Data* data1 = Gearef(context, StackTest)->data1;
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto pop2Test1StackTestImpl3(context, stackTest, data, data1, stack, next);
}

__code insertTest3StackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    StackTest2* stackTest2 = createStackTest2Impl(context);
    String* str = NEW(String);
    str->size = 100;
    Gearef(context, StackTest2)->stackTest2 = (union Data*) stackTest2;
    Gearef(context, StackTest2)->stack = stack;
    Gearef(context, StackTest2)->data1 = (union Data*)  (union Data*)str;
    Gearef(context, StackTest2)->next = C_pop2TestStackTestImpl3;
    goto meta(context, stackTest2->insertTest1);
}

__code insertTest3StackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto insertTest3StackTestImpl3(context, stackTest, stack, next);
}

__code insertTest4StackTestImpl3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    StackTest2* stackTest2 = createStackTest2Impl(context);
    String* str = NEW(String);
    str->size = 100;
    Gearef(context, StackTest2)->stackTest2 = (union Data*) stackTest2;
    Gearef(context, StackTest2)->stack = stack;
    Gearef(context, StackTest2)->data1 = (union Data*)  (union Data*)str;
    Gearef(context, StackTest2)->next = C_pop2TestStackTestImpl3;
    goto meta(context, stackTest2->insertTest1);
}
__code insertTest4StackTestImpl3_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto insertTest4StackTestImpl3(context, stackTest, stack, next);
}

__code pop2Test1StackTestImpl3_1_stub(struct Context* context) {
	StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
	Data* data = Gearef(context, Stack)->data;
	Data* data1 = Gearef(context, Stack)->data1;
	Stack* stack = Gearef(context, StackTest)->stack;
	enum Code next = Gearef(context, StackTest)->next;
	goto pop2Test1StackTestImpl3(context, stackTest, data, data1, stack, next);
}

# Gears コンストラクタの自動生成

#implキーワードとすり替えられる
- 基本的にはtrans_impl.plで実装していたルーチンの移植

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18


            } elsif(/^#impl "(.*)"/) {
              next unless ($implInterfaceInfo->{genConstructor});

              my $constructInterface = {
                                         name => $implInterfaceInfo->{interface},
                                         path => $headerNameToInfo->{$implInterfaceInfo->{interface}}->{path}
                                       };

              my $constructImpl      = {
                                        name => $implInterfaceInfo->{implementation},
                                         path => $headerNameToInfo->{$implInterfaceInfo->{implementation}}->{path}
                                       };

              unless ($constructImpl->{path}) {
                warn "[WARN] Not found $constructImpl->{name}.h";
              }
              print $fd Gears::Stub->generate_constructor($constructInterface, $constructImpl);
              next;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20


#include "../../../context.h"
#include <stdio.h>

#include "/Users/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/examples/pop_and_push/String.h"

StackTest* createStackTestImpl3(struct Context* context) {
    struct StackTest* stackTest  = &ALLOCATE(context, StackTest)->StackTest;
    struct StackTestImpl3* StackTestImpl3 = &ALLOCATE(context, StackTestImpl3)->StackTestImpl3;
    stackTest->stackTest = (union Data*)StackTestImpl3;
    stackTest->stack = NULL;
    stackTest->data = NULL;
    stackTest->data1 = NULL;
    stackTest->insertTest1 = C_insertTest1StackTestImpl3;
    stackTest->insertTest2 = C_insertTest2StackTestImpl3;
    stackTest->insertTest3 = C_insertTest3StackTestImpl3;
    stackTest->insertTest4 = C_insertTest4StackTestImpl3;
    stackTest->pop2Test = C_pop2TestStackTestImpl3;
    stackTest->pop2Test1 = C_pop2Test1StackTestImpl3;
    return stackTest;
}

# 悩みどころ

# 直接gotoしたいのに引数が落とされる

こうすると

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


__code pop2Test3(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    union Data* data = (union Data*)str;
    union Data* data1 = (union Data*)str1;

    goto pop2Test1(stackTest, data, data1);
}

こうなるもの

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


__code pop2Test3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next) {
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    union Data* data = (union Data*)str;
    union Data* data1 = (union Data*)str1;

    goto meta(context, C_pop2Test1StackTestImpl3);
}

出力があってないという話らしい

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


__code pop2Test3(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(union Data* data, union Data* data1, ...)) {
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    data = (union Data*)str;
    data1 = (union Data*)str1;

    goto pop2Test1(stackTest, data, data1);
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


__code pop2Test3(struct Context *context,struct StackTestImpl3* stackTest, struct Stack* stack, enum Code next,union Data **O_data,union Data **O_data1) {
  Data* data  __attribute__((unused))  = *O_data;
  Data* data1  __attribute__((unused))  = *O_data1;
    String* str = NEW(String);
    str->size = 200;
    String* str1 = NEW(String);
    str1->size = 300;
    data = (union Data*)str;
    data1 = (union Data*)str1;

    goto meta(context, C_pop2Test1StackTestImpl3);
}

これは書き方の問題っぽい…….

# Copy on Writeの実装

InterfaceのDataGearに書き込みに行くタイミングでコピーしたい気がする
- 誰が書き込んでいるCodeGearなのかの特定がしたい
- CodeGear内でのInterfaceへの再代入を禁止する
  - 再代入したい場合は新しいGearを作って差し替えたい
  - ここは別のメタ計算を埋め込みたい

2020/09/08

2020/09/08

# 研究目的

# 最近

# Gears Interface

# 名前空間の実装

# 基本ルール

# 実際に書く

# ヘッダ

# 実装

# 変換後

# Gears コンストラクタの自動生成

# 悩みどころ

# 直接gotoしたいのに引数が落とされる

# Copy on Writeの実装