# 研究目的

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

# 今週

対島を救った
シス管関連
- スイッチのconfigをいい感じにパースするスクリプトを書いていた
- あとは後輩と仲良く作業とかakatsukiのとか
Gears関連
- 自分で書いてたほうのPerlスクリプトのリファクタ
- generate_stub.plの修正
Haskell,Rustの勉強 …

# シス管関連

Perlのライブコーディングをやってました
https://gitlab.ie.u-ryukyu.ac.jp/k198584/switchConf2parsedcsv
- システム更新時にクリティカルなポートの一覧をだすくん

# Gears関連

# 方針

localCodeに限らずmetaにgotoするのを強制する
generate_stub側の修正を頑張る
- とりあえずparallelを優先にして、xv6はあとで

# クリティカルな問題

 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


__code pop2Test_StackTestImpl(struct StackTestImpl* stackTest, struct Stack* stack, __code next(...)) {
  goto stack->pop2(pop2Test1_StackTestImpl);
}

__code pop2Test3_StackTestImpl(struct StackTestImpl* stackTest, struct Stack* stack, __code next(...)) {
  String* str = NEW(String);
  str->size = 200;
  String* str1 = NEW(String);
  str1->size = 300;
  goto pop2Test1_StackTestImpl(stackTest, (union Data*)str, (union Data*)str1);
}


__code pop2Test1_StackTestImpl(struct StackTestImpl* 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(...);
}

__code pop2Test1_StackTestImpl_stub(struct Context* context) {
  struct StackTestImpl* stackTest = 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 pop2Test1_StackTestImpl(context, stackTest, data, data1, stack, next);
}

# generate_stub.pl

各.cbcごとに.cを生成するくん
- スタブを生成する
- generate_stub.pl -o hoge.c hoge.cbcみたいに使う
  - なかでパースされるのがhoge.cbcだけとは限らない

# リファクタリング

とりあえず巨大なelseを落とす

 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


     if ($typeName eq $implementation) {
         # get implementation
         $dataGearName{$codeGearName} .= "\t$typeName* $varName = ($typeName*)GearImpl($context_name, $interface, $varName);\n";
-    } else {
-        # interface var
-        for my $ivar (keys %{$var{$interface}}) {
-            #  input data gear field
-            if ($varName eq $ivar) {
-                if ($typeName eq $var{$interface}->{$ivar}) {
-                    if ($output) {
-                        $dataGearName{$codeGearName} .= "\t$typeName$ptrType* O_$varName = &Gearef($context_name, $interface)->$varName;\n";
-                        $outputVar{$codeGearName} .= "\t$typeName$ptrType $varName  __attribute__((unused))  = *O_$varName;\n";
-                        return 1;
-                    }
-                    $dataGearName{$codeGearName} .= "\t$typeName$ptrType $varName = Gearef($context_name, $interface)->$varName;\n";
+        return 1;
+    }
+    # interface var
+    for my $ivar (keys %{$var{$interface}}) {
+        #  input data gear field
+        if ($varName eq $ivar) {
+            if ($typeName eq $var{$interface}->{$ivar}) {
+                if ($output) {
+                    $dataGearName{$codeGearName} .= "\t$typeName$ptrType* O_$varName = &Gearef($context_name, $interface)->$varName;\n";
+                    $outputVar{$codeGearName} .= "\t$typeName$ptrType $varName  __attribute__((unused))  = *O_$varName;\n";
                     return 1;

# .hと.cbcのリスト

インターフェイスを読み込む必要が出てくるので、最初にディレクトリ下を再帰的に.hと.cbcを回収しにいく
- 一時ファイルにしようかなと思ったが、そんなに遅くなかったので実行時に最初に呼び出す方法に

 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


sub create_interface_name_to_header_path {
    my $search_root = shift;
    my $files = Gears::Util->find_headers_from_path($search_root);
    my $interface_name2headerpath = {};

    for my $file (@{$files}) {
      if ($file =~ m|/(\w+)\.\w+$|) {
        my $file_name = $1;
        $interface_name2headerpath->{$file_name} = $file;
      }
    }

    return $interface_name2headerpath;
}

sub create_cbc_name_to_source_path {
  my $search_root = shift;
  my $files = Gears::Util->find_cbc_sources_from_path($search_root);

  my $cbc_name2_source_path = {};
  for my $file (@{$files}) {
    my $cbc_name = basename $file;
    $cbc_name =~ s/\.cbc//;
    push(@{$cbc_name2_source_path->{$cbc_name}},$file);
  }
  return $cbc_name2_source_path;
}

なんとこっそりモジュール化しつつある

 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


package Gears::Util;
use strict;
use warnings;
use Carp qw/croak/;
use File::Find;

sub find_cbc_sources_from_path {
  my $class = shift;
  my $find_path = shift // ".";

  my @files;
  find( { wanted => sub { push @files, $_ if /\.cbc/ }, no_chdir => 1 }, $find_path);

  return \@files;
}

sub find_headers_from_path {
  my $class = shift;
  my $find_path = shift // ".";

  my @files;
  find( { wanted => sub { push @files, $_ if /\.(?:h|dg)/ }, no_chdir => 1 }, $find_path);

  return \@files;
}

getDataGearの安定感が向上しました

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


            } elsif(/^#interface "(.*)"/) {
                # use interface
                my $interfaceHeader = $1;
                 next if ($interfaceHeader =~ /context.h/);
-                if (-f $interfaceHeader) {
-                    &getDataGear("$interfaceHeader");
-                    &getCodeGear("$interfaceHeader");
-                } else {
-                  if ($filename =~ /([\w\/]+)\/(.+)$/) {
-                    $interfaceHeader = "$1/$interfaceHeader";
-                    if (-f $interfaceHeader) {
-                        &getDataGear("$interfaceHeader");
-                        &getCodeGear("$interfaceHeader");
-                    }
-                  }
+                $interfaceHeader =~ m|(\w+)\.\w+$|; #remove filename extention
+                my $interfaceName = $1;
+                $call_interfaces{$filename}->{$interfaceName} = 1;
+                if (exists $interface_name_to_header_paths->{$interfaceName}) {
+                    &getDataGear($interface_name_to_header_paths->{$interfaceName});
+                    &getCodeGear($interface_name_to_header_paths->{$interfaceName});
                 }

# 呼び出しもとのinterfaceの特定,使うinterfaceをuseしているかどうか

今週実装予定です
getDataGearで探すと良さそう
- 今まではgetDataGearでは__codeの引数などは見てなかったので、結構修正する必要はありそう…
- interfaceのパーサーは既に実装しているので、それを呼び出すのが早いかもしれない

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


            } elsif(/^#interface "(.*)"/) {
                # use interface
                my $interfaceHeader = $1;
                next if ($interfaceHeader =~ /context.h/);
                $interfaceHeader =~ m|(\w+)\.\w+$|; #remove filename extention
                my $interfaceName = $1;
                $call_interfaces{$filename}->{$interfaceName} = 1;
                if (exists $interface_name_to_header_path->{$interfaceName}) {
                    &getDataGear($interface_name_to_header_path->{$interfaceName});
                    &getCodeGear($interface_name_to_header_path->{$interfaceName});
                }
            } elsif (/^\_\_code (\w+)\((.*)\)(.*)/) {
                my $codeGearName = $1;
                if ($filename =~ /^(.*)\/(.*)/) {
                    $codeGearName = "$1/$codeGearName";
                }
                if ( -f "$codeGearName.cbc") {
                    &getCodeGear("$codeGearName.cbc");
                }
            }
            next;

# implのname space

#implで指定したInterfaceと同名の__codeが対象
- generate_stubのタイミングで名前が変わる

 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


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

#impl "Stack.h"
//include "Node.h"
// typedef struct SingleLinkedStack {
//     struct Element* top;
// } SingleLinkedStack;


__code clear(struct SingleLinkedStack* stack,__code next(...)) {
    stack->top = NULL;
    goto next(...);
}

__code push(struct SingleLinkedStack* stack, union Data* data, __code next(...)) {
    Element* element = new Element();
    element->next = stack->top;
    element->data = data;
    stack->top = element;
    goto next(...);
}

__code pop(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
    if (stack->top) {
        data = stack->top->data;
        stack->top = stack->top->next;
    } else {
        data = NULL;
    }
    goto next(data, ...);
}

__code pop2(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) {
    if (stack->top) {
        data = stack->top->data;
        stack->top = stack->top->next;
    } else {
        data = NULL;
    }
    if (stack->top) {
        data1 = stack->top->data;

これが生成される

コンストラクタは書けば優先される(基本は自動生成)

 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 <stdio.h>

//include "Node.h"
// typedef struct SingleLinkedStack {
//     struct Element* top;
// } SingleLinkedStack;

Stack* createSingleLinkedStack(struct Context* context) {
    struct Stack* stack = &ALLOCATE(context, Stack)->Stack;
    struct SingleLinkedStack* singleLinkedStack = &ALLOCATE(context, SingleLinkedStack)->SingleLinkedStack;
    stack->stack = (union Data*)singleLinkedStack;
    singleLinkedStack->top = NULL;
    stack->push = C_pushSingleLinkedStack;
    stack->pop  = C_popSingleLinkedStack;
    stack->pop2  = C_pop2SingleLinkedStack;
    stack->get  = C_getSingleLinkedStack;
    stack->get2  = C_get2SingleLinkedStack;
    stack->isEmpty = C_isEmptySingleLinkedStack;
    stack->clear = C_clearSingleLinkedStack;
    return stack;
}

void printStack1(union Data* data) {
    struct Node* node = &data->Element.data->Node;
    if (node == NULL) {
        printf("NULL");
    } else {
        printf("key = %d ,", node->key);
        printStack1((union Data*)data->Element.next);
    }
}

void printStack(union Data* data) {
    printStack1(data);
    printf("\n");
}

__code clearSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack,enum Code next) {
    stack->top = NULL;
    context->before = C_clearSingleLinkedStack;
    goto meta(context, next);
}

__code clearSingleLinkedStack_stub(struct Context* context) {
        SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack);
        enum Code next = Gearef(context, Stack)->next;
        goto clearSingleLinkedStack(context, stack, next);
}

2020/08/18

2020/08/18

# 研究目的

# 今週

# シス管関連

# Gears関連

# 方針

# クリティカルな問題

# generate_stub.pl

# リファクタリング

# .hと.cbcのリスト

# 呼び出しもとのinterfaceの特定,使うinterfaceをuseしているかどうか

# implのname space