2020/07/14

2020/07/14

# 研究目的

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

# 進捗

  • CbC/Gears勉強会した
  • Raku(Perl6)の復習
    • わりと忘れている…..
  • xv6の書き換え作業
  • シス管関連
    • テスト用ldap環境をDockerでつくっていた
    • gitlabのプロキシ関連
    • NetlifyCMSが使えるように!
  • インターネットの人に煽られて Scala(akka)とHaskellやってます

# CbC勉強会

# Raku

# xv6の書き換え

  • cbc_readでスタックが積まれていた
    • bl命令に変換されてる…..
    • blはサブルーチンコールと対応していて、retしないといけなくなってしまう

# 対応するコード

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
__ncode cbc_read(__code (*next)(int ret)){
    struct file *f;
    int n;
    char *p;

    if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
        goto next(-1);
    }
    goto cbc_fileread(f, p, n, 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
11          LDR     r1, =edata_entry
(gdb) b cbc_read
Breakpoint 1 at 0x800236b8: file /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/sysfile.c, line 85.
(gdb) c
Continuing.

Breakpoint 1, cbc_read (next=0x800231b4 <cbc_ret>) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/sysfile.c:85
85          if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
(gdb) n
88          goto cbc_fileread(f, p, n, next);
(gdb) x/20i $pc
=> 0x80023730 <cbc_read+136>:   ldr     r3, [r11, #-28] ; 0xffffffe4
   0x80023734 <cbc_read+140>:   str     r3, [r11, #-8]
   0x80023738 <cbc_read+144>:   ldr     r3, [r11, #-36] ; 0xffffffdc
   0x8002373c <cbc_read+148>:   str     r3, [r11, #-12]
   0x80023740 <cbc_read+152>:   ldr     r3, [r11, #-32] ; 0xffffffe0
   0x80023744 <cbc_read+156>:   str     r3, [r11, #-16]
   0x80023748 <cbc_read+160>:   ldr     r3, [r11, #-40] ; 0xffffffd8
   0x8002374c <cbc_read+164>:   str     r3, [r11, #-20] ; 0xffffffec
   0x80023750 <cbc_read+168>:   ldr     r3, [r11, #-20] ; 0xffffffec
   0x80023754 <cbc_read+172>:   ldr     r2, [r11, #-16]
   0x80023758 <cbc_read+176>:   ldr     r1, [r11, #-12]
   0x8002375c <cbc_read+180>:   ldr     r0, [r11, #-8]
   0x80023760 <cbc_read+184>:   bl      0x80020f5c <cbc_fileread>
   0x80023764 <cbc_read+188>:   nop                     ; (mov r0, r0)
   0x80023768 <cbc_read+192>:   sub     sp, r11, #4
   0x8002376c <cbc_read+196>:   pop     {r11, pc}
   0x80023770 <sys_read>:       push    {r11, lr}
   0x80023774 <sys_read+4>:     add     r11, sp, #4
   0x80023778 <sys_read+8>:     sub     sp, sp, #16
   0x8002377c <sys_read+12>:    sub     r3, r11, #8
(gdb) bt
#0  cbc_read (next=0x800231b4 <cbc_ret>) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/sysfile.c:88
#1  0x800344f0 in trap_swi () at /mnt/dalmore-home/one/src/cbcxv6/src/trap_asm.S:30
#2  0x000019dc in ?? ()
Backtrace stopped: previous frame identical to this frame (corrupt stack?)
  • コンパイラのバグっぽい気もするけれど、追求するべきかは悩む(それよりInterface化したい)

# Interface化

  • readをitnerface化中
    • とりあえずコピってくるとこは終わった
    • goto nextするときの引数をKernelRetinterfaceに書き込む必要がある
      • アセンブラのretを呼び出すinterface
      • nextの値は自分自身のinterfaceに呼び出されてしまう
  • nextの引数はアノテーション的なものか記法で解決したい
1
2
3
4
    goto next[KernelRet](ret,...); ....?
    
    @KernelRet 
    goto next(ret,...);

# interface化

  • 全部同じファイルにしたので絶対にこのままでは動かない
    • グローバル変数はkernelのcontextに積みたい
      • どこで積むかは別途考える(ヘッダファイル化する?)
  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
#include "../context.h"
#interface "ReadSyscall.h"
#interface "KernelRet.h"

// ----
// typedef struct ReadSyscallImpl <Type, Isa> impl ReadSyscall {
//   __code next(....);
// } ReadSyscallImpl;
// ----

ReadSyscall* createReadSyscallImpl(struct Context* cbc_context) {
    struct ReadSyscall* read_syscall  = new ReadSyscall();
    struct ReadSyscallImpl* read_syscall_impl = new ReadSyscallImpl();
    read_syscall->read_syscall = (union Data*)read_syscall_impl;
    read_syscall->consoleread = C_consolereadReadSyscallImpl;
    read_syscall->consoleread1 = C_consoleread1ReadSyscallImpl;
    read_syscall->consoleread2 = C_consoleread2ReadSyscallImpl;
    read_syscall->piperead = C_pipereadReadSyscallImpl;
    read_syscall->piperead1 = C_piperead1ReadSyscallImpl;
    read_syscall->piperead2 = C_piperead2ReadSyscallImpl;
    read_syscall->piperead3 = C_piperead3ReadSyscallImpl;
    read_syscall->fileread = C_filereadReadSyscallImpl;
    read_syscall->fileread1 = C_fileread1ReadSyscallImpl;
    return read_syscall;
}

__code consolereadReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct inode* ip, char* dst, int n, __code next(int ret, ...)) {
    uint target;

    iunlock(ip);

    //target = n;
    acquire(&input.lock);

    if (n > 0) {
        goto read_syscall->consoleread2(...);
    }

    goto read_syscall->consoleread1(...);
}

__code consoleread1ReadSyscallImpl(struct ReadSyscallImpl* read_syscall,int n, int target, char* dst, struct inode* ip,  __code next(...)) {
    int cont = 1;
    int c = input.buf[input.r++ % INPUT_BUF];

    if (c == C('D')) {  // EOF
        if (n < target) {
            // Save ^D for next time, to make sure
            // caller gets a 0-byte result.
            input.r--;
        }
        cont = 0;
    }

    *dst++ = c;
    --n;

    if (c == '\n') {
        cont = 0;
    }

    if (cont == 1) {
        if (n > 0) {
            goto cbc_sleep(&input.r, &input.lock, read_syscall->consoleread2);
        }
    }

    release(&input.lock);
    ilock(ip);
    goto next(target - n);
}

__code consoleread2ReadSyscallImpl(struct ReadSyscallImpl* read_syscall,struct inode* ip, __code next(...)) {
    if (input.r == input.w) {
        if (proc->killed) {
            release(&input.lock);
            ilock(ip);
            KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
            goto kernel_ret->cbc_return(-1);
        }
       goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2);
    }
    goto read_sycall->consoleread1();
}

__code pipereadReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct pipe* p,char* addr, int n,  __code next(int ret,...)) {

    goto next(ret,...);
}

__code piperead1ReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct pipe* p, __code next(int ret,...)) {
    if (p->nread == p->nwrite && p->writeopen){
        if(proc->killed){
            release(&p->lock);
            KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
            goto kernel_ret->cbc_return(-1);
        }
        goto cbc_sleep(&p->nread, &p->lock, cbc_piperead1);
    }
    goto read_syscall->piperead2(...);
}

__code piperead2ReadSyscallImpl(struct ReadSyscallImpl* read_syscall, int i, int n, struct pipe* p, char* addr, __code next(...)) {
    if (i < n && !(p->nread == p->nwrite)) {
        addr[i] = p->data[p->nread++ % PIPESIZE];
        i ++;
        goto read_syscall->piperead2(i,n, p, addr,next);
    }
    //proc->cbc_arg.cbc_console_arg.p = p;
    goto cbc_wakeup(&p->nwrite, cbc_piperead3);  //DOC: piperead-wakeup
}

__code piperead3ReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct pipe* p, int i, __code next(int ret,...)) {
    release(&p->lock);
    KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
    goto kernel_ret->cbc_return(-1);
}

__code filereadReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct file* f, char* addr, int n, __code next(int ret, ...)) {
    if (f->readable == 0) {
        ret = -1;
        KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
        goto kernel_ret->cbc_return(ret);
    }

    if (f->type == FD_PIPE) {
        goto read_syscall->piperead(f->pipe, addr, n, next);
    }

    if (f->type == FD_INODE) {
        ilock(f->ip);
        goto read_syscall->cbc_readi(f->ip, addr, f->off, n, readsys_call->fileread1);
    }

    goto cbc_panic("fileread");
}

__code fileread1ReadSyscallImpl(struct ReadSyscallImpl* read_syscall, struct file* f, int ret, __code next(ret, ...)) {
    if (ret > 0)
        f->off += ret;
    iunlock(f->ip);
    KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
    goto kernel_ret->cbc_return(ret);
}

# panic

  • 全部Interface化するならこのあたりも必要
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
__ncode cbc_panic (char *s)
{
    cli();

    cons.locking = 0;

    cprintf("cpu%d: panic: ", cpu->id);

    show_callstk(s);
    panicked = 1; // freeze other CPU

    while (1)
        ;
}

panickedはファイル内のグローバル変数

  • kernel_contextとアドレスを共有する

# interface化

  • 先月書いてたらしい
1
2
3
4
5
typedef struct Err <Type, Impl> {
  __code error(Impl* err, int err_code, __code next(...));
  __code panic(Impl* err, char* msg);
  __code next(...);
} Err;
1
2
3
4
typedef struct KernelError <Type, Isa> impl Err {
  __code infinity_loop(Type* err, __code next(...));
  __code next(...);
} KernelError;
 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
#include "param.h"
#include "proc.h"
#interface "Err.h"

// ----
// typedef struct KernelError <Type, Isa> impl Error {
//   __code infinity_loop(Type* error, next(...));
// } KernelError;
// ----

Err* createKernelError(struct Context* cbc_context) {
    struct Err* err  = new Err();
    struct KernelError* kernel_error = new KernelError();
    err->err = (union Data*)kernel_error;
    kernel_error->err = (union Data*)kernel_error;
    kernel_error->infinity_loop = C_infinity_loopKernelError;
    err->error = C_errorKernelError;
    err->panic = C_panicKernelError;
    return err;
}

__code infinity_loopKernelError(struct KernelError* err, __code next(...)) {
  goto next(...);
}

__code errorKernelError(struct KernelError* err, int err_code, __code next(...)) {

    goto next(...);
}

__code panicKernelError(struct KernelError* err, char* msg) {
    cli();
    cons.locking = 0;

    cprintf("cpu%d: panic: ", cpu->id);

    show_callstk(msg);
    panicked = 1; // freeze other CPU

    goto infinity_loopKernelError(err, err->inifinity_loop);
}

# シス管関連

  • 詳しくは明日…

# LDAP

  • さまざまなアプリケーションを実装する時にLDAPがネック

    • 大学でLDAP本番環境に接続するという方法もあるが…..
  • akatsukiのリプレイスもあるので実装したい

    • akatsukiの時に使っていたDockerfileは使えない
    • 残念ながらyumからOpenLDAPが削除されている
    • ubuntuでopenldapをapt getすると対話型のTUIが起動されて辛く厳しい
  • https://github.com/osixia/docker-openldap

    • 起動するとこまではいけたけれど、LDAPツリーが意図していたものと異なる
    • その上seedでいれたldifが反映されない…..

# gitlab

Licensed under CC BY-NC-SA 4.0
comments powered by Disqus
Built with Hugo
Theme Stack designed by Jimmy