2020/07/07

2020/07/07

# 研究目的

# 研究目的

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

# 進捗

  • xv6軽く読んだ
  • generate_stubの修正
  • xv6の書き換え
    • systemcall呼び出し
    • read systemcall
    • プロセス関連
      • wakeup
      • sleep

# Gears関連

# 問答無用でgoto metaに変換される問題

  • 変換はgenerate_stub.plでやっていて、ここの処理が問題
1
2
3
4
5
6
 } elsif (/extern\s+_\_code\s+(\w+)\((.*)\)/) {
    $localCode{$1} = 1;
 } elsif (/^\s\s*_\_code\s+(\w+)\((.*)\)(.*)/) {
    $localCode{$1} = 1;
 } elsif (/^\s\s*_\_code  *\(\s*\*\s*(\w+)\)\((.*)\)(.*)/) {
    $localCode{$1} = 1;
  • __code(先頭にスペース)があったものはlocalCodeにカウントされる
    • localCodeはhash
    • externの部分は今週追加したとこ

%localCodeはgotoが来たタイミングで中身が確認される

  • goto先がlocalCodeだったらgoto metaにしない
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
            } elsif (/^(.*)goto (\w+)\((.*)\);/) {
                # handling goto statement
                # convert it to the meta call form with two arugments, that is context and enum Code
                my $prev = $1;
                my $next = $2;
                my @args = split(/,/, $3);
                my $v = 0;
                if (defined $localCode{$next}) {
                    print $fd $_; next;
                }
                for my $n ( @{$dataGearVar{$codeGearName}} ) {
                    # continuation arguments
                    $v = 1  if ( $n eq $next);
                }

デバッグした

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
  DB<33> c
main::generateDataGear(/mnt/dalmore-home/one/src/cbcxv6/src/gearsTools/generate_stub.pl:650):
650:                    if (defined $localCode{$next}) {
  DB<33> p $_
    goto trapret();

  DB<34> print Dumper \%localCode;
$VAR1 = {
          'HASH(0x29947c0)' => undef
        };
  • %localCodeの値がわけわからんものになっている
1
2
3
4
5
6
7
             } elsif (/^\_\_code (\w+)\((.*)\)(.*)/) {
                 $inCode = 1;
-                %localCode = {};
+                $localCode{$inCode} = {};
                 %localVarType = {};
                 $codeGearName = $1;
                 my $args = $2;
  • Perlだとハッシュにハッシュリファレンスを代入するとリファレンスの文字列表記がキーになるなしい…
    • ということで従来の実装だとlocalCodeが死んでいてた

# xv6の書き換え

  • 読み会やりつつ書き換えていく
  • システムコールを中心に書き換える
  • Interfaceへの変換は素朴にやる
    • __ncodeを愚直に書き換えていく

# システムコール呼び出し

  • trapした時に呼ばれるハンドラで関数呼び出しをしてシステムコールを読んでいる
    • 部分的にスタックがあるので色々と不便
    • とりあえずスタックを追放する路線で実装をすすめる

# trap_asm.S

  • 書き換えたcbc_swi_handlerにBL
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
# handle SWI, we allow nested SWI
trap_swi:
    # build trapframe on the stack
    STMFD   sp!, {r0-r12, r14}  // save context
    MRS     r2, spsr            // copy spsr to r2
    STMFD   r13!, {r2}          // save r2(spsr) to the stack
    STMFD   r13!, {r14}         // save r14 again to have one uniform trapframe
    STMFD   r13, {sp, lr}^      // save user mode sp and lr
    SUB     r13, r13, #8

    # call traps (trapframe *fp)
    MOV     r0, r13             // copy r13_svc to r0
    BL      cbc_swi_handler         // branch to the isr_swi

# trap.cbc

  • もともとのコード
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
// trap routine
void swi_handler (struct trapframe *r)
{
    if (proc->killed)
        exit();
    proc->tf = r;
    syscall ();
    if (proc->killed)
        exit();
}
  • exitするのはsyscall()の次の継続でやる路線にすれば書き換えられそう
  • goto metaでkernel使いたいときはとりあえず愚直に書く
    • SyscallDispatchを毎回初期化するのめんどいので別の場所で初期化したい
    • なぜかコンストラクタをexternしないと関数呼び出しが落とされる
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
extern SyscallDispatch* createSyscallDispatchImpl(struct Context*);
extern KernelRet* createKernelRetImpl(struct Context*);

__ncode cbc_swi_handler(struct trapframe* r) {
    struct Context*         kernel                = &kernel_context->context;
    struct SyscallDispatch* syscall_dispatch      = createSyscallDispatchImpl(kernel);

    if (proc->killed) {
        struct KernelRet* kernelret = createKernelRetImpl(kernel);
        goto meta(kernel, kernelret->exit);
    }
    proc->tf = r;
    goto meta(kernel, syscall_dispatch->dispatch);
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
Breakpoint 1, cbc_swi_handler (r=0x87fe2fb8) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/trap.c:17
17          struct Context* kernel       = &kernel_context->context;
(gdb) n
18          struct Syscall* syscall      = createSyscallImpl(kernel);
(gdb) p kernel
$1 = (struct Context *) 0x87ffd000
(gdb) n
20          if (proc->killed) {
(gdb) p syscall
$2 = (struct Syscall *) 0x87fe2fb4
(gdb) p *syscall
$3 = {syscall = 0x0, dispatch = C_allocinode, next = C_copyuvm_loop_bad}
(gdb) quit
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
17          struct Context* kernel       = &kernel_context->context;
(gdb) x/20i $pc
=> 0x800245e4 <cbc_swi_handler+16>:     ldr     r3, [pc, #176]  ; 0x8002469c <swi_handler+16>
   0x800245e8 <cbc_swi_handler+20>:     ldr     r3, [r3]
   0x800245ec <cbc_swi_handler+24>:     str     r3, [r11, #-8]
   0x800245f0 <cbc_swi_handler+28>:     ldr     r3, [r11, #-8]
   0x800245f4 <cbc_swi_handler+32>:     ldr     r3, [r3, #28]
   0x800245f8 <cbc_swi_handler+36>:     add     r3, r3, #40     ; 0x28
   0x800245fc <cbc_swi_handler+40>:     ldr     r3, [r3]
   0x80024600 <cbc_swi_handler+44>:     ldr     r3, [r3]
   0x80024604 <cbc_swi_handler+48>:     str     r3, [r11, #-12]
   0x80024608 <cbc_swi_handler+52>:     ldr     r3, [pc, #144]  ; 0x800246a0 <swi_handler+20>
   0x8002460c <cbc_swi_handler+56>:     ldr     r3, [r3]
   0x80024610 <cbc_swi_handler+60>:     ldr     r3, [r3, #36]   ; 0x24
   0x80024614 <cbc_swi_handler+64>:     cmp     r3, #0
   0x80024618 <cbc_swi_handler+68>:     beq     0x80024660 <cbc_swi_handler+140>
   0x8002461c <cbc_swi_handler+72>:     ldr     r3, [r11, #-8]
   0x80024620 <cbc_swi_handler+76>:     ldr     r3, [r3, #28]
   0x80024624 <cbc_swi_handler+80>:     add     r3, r3, #20
   0x80024628 <cbc_swi_handler+84>:     ldr     r3, [r3]
   0x8002462c <cbc_swi_handler+88>:     ldr     r3, [r3]
   0x80024630 <cbc_swi_handler+92>:     str     r3, [r11, #-16]

# systemcall dispatch

  • dispatchするだけ
1
2
3
4
typedef struct SyscallDispatch <Type, Impl> {
  __code dispatch(Impl* syscall_dispatch, __code next(...));
  __code next(....);
} SyscallDispatch;
1
2
3
typedef struct SyscallDispatchImpl <Type, Isa> impl SyscallDispatch {
  __code next(....);
} SyscallDispatchImpl;
  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
#include "types.h"
#include "defs.h"
#include "param.h"
#include "memlayout.h"
#include "mmu.h"
#include "proc.h"
#include "arm.h"
#include "syscall.h"

#include "../../kernel.h"
#interface "SyscallDispatch.h"
#interface "KernelRet.h"

extern int sys_chdir(void);
extern int sys_close(void);
extern int sys_dup(void);
extern int sys_exec(void);
extern int sys_exit(void);
extern int sys_fork(void);
extern int sys_fstat(void);
extern int sys_getpid(void);
extern int sys_kill(void);
extern int sys_link(void);
extern int sys_mkdir(void);
extern int sys_mknod(void);
extern int sys_open(void);
extern int sys_pipe(void);
extern int sys_read(void);
extern int sys_sbrk(void);
extern int sys_sleep(void);
extern int sys_unlink(void);
extern int sys_wait(void);
extern int sys_write(void);
extern int sys_uptime(void);

extern __code cbc_read(__code(*)(int));


static int (*syscalls[])(void) = {
        [SYS_fork]    =sys_fork,
        [SYS_exit]    =sys_exit,
        [SYS_wait]    =sys_wait,
        [SYS_pipe]    =sys_pipe,
        [SYS_read]    =sys_read,
        [SYS_kill]    =sys_kill,
        [SYS_exec]    =sys_exec,
        [SYS_fstat]   =sys_fstat,
        [SYS_chdir]   =sys_chdir,
        [SYS_dup]     =sys_dup,
        [SYS_getpid]  =sys_getpid,
        [SYS_sbrk]    =sys_sbrk,
        [SYS_sleep]   =sys_sleep,
        [SYS_uptime]  =sys_uptime,
        [SYS_open]    =sys_open,
        [SYS_write]   =sys_write,
        [SYS_mknod]   =sys_mknod,
        [SYS_unlink]  =sys_unlink,
        [SYS_link]    =sys_link,
        [SYS_mkdir]   =sys_mkdir,
        [SYS_close]   =sys_close,
};


static __code (*cbccodes[])(__code (*)(int)) = {
       [SYS_cbc_read]  = cbc_read,
};



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

SyscallDispatch* createSyscallDispatchImpl(struct Context* cbc_context) {
    struct SyscallDispatch* syscall_dispatch  = new SyscallDispatch();
    struct SyscallDispatchImpl* syscall_dispatch_impl = new SyscallDispatchImpl();
    syscall_dispatch->syscall_dispatch = (union Data*)syscall_dispatch_impl;
    syscall_dispatch->dispatch = C_dispatchSyscallDispatchImpl;
    return syscall_dispatch;
}

__code dispatchSyscallDispatchImpl(struct SyscallDispatchImpl* syscall_dispatch, __code next(...)) {
    KernelContext* kcontext = kernel_context;
    kcontext->now_proc = proc;
    proc->cbc_context.proc = proc;

    int num = proc->tf->r0;

    if (num == 5)
        num = 22;

    struct KernelRet* kernelRet = createKernelRetImpl(cbc_context);

    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
        proc->cbc_arg.cbc_console_arg.num = num;
        __code *syscalls = kcontext->syscalls;

        goto (cbccodes[num])(cbc_ret);
        //goto meta(&proc->cbc_context, cbccodes[num]);
    }


    if((num > 0) && (num < NELEM(syscalls)) && syscalls[num]) {
        int ret = syscalls[num]();

        // in ARM, parameters to main (argc, argv) are passed in r0 and r1
        // do not set the return value if it is SYS_exec (the user program
        // anyway does not expect us to return anything).

        goto kernelRet->cbc_return(ret);

    }

    cprintf("%d %s: unknown sys call %d\n", proc->pid, proc->name, num);
    goto kernelRet->cbc_return(-1);
}

# kernelRet

  • swchやexitなどのアセンブラで記述されたやつのInterface
1
2
3
4
5
6
typedef struct KernelRet <Type, Impl> {
  __code cbc_return(Impl* kernelRet, int ret, __code next(...));
  __code exit(Impl* kernelRet, __code next(...));
  __code swtch(Impl* kernelRet, __code next(...));
  __code next(....);
} KernelRet;
1
2
3
typedef struct KernelRetImpl <Type, Isa> impl KernelRet {
  __code next(....);
} KernelRetImpl;
 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
#include "types.h"
#include "arm.h"
#include "param.h"
#include "syscall.h"
#include "proc.h"
#interface "KernelRet.h"

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

KernelRet* createKernelRetImpl(struct Context* cbc_context) {
    struct KernelRet* kernelRet  = new KernelRet();
    struct KernelRetImpl* kernelRet_impl = new KernelRetImpl();
    kernelRet->kernelRet = (union Data*)kernelRet_impl;
    kernelRet->cbc_return = C_cbc_returnKernelRetImpl;
    kernelRet->exit = C_exitKernelRetImpl;
    kernelRet->swtch = C_swtchKernelRetImpl;
    return kernelRet;
}

extern __code trapret(void);

__code cbc_returnKernelRetImpl(struct KernelRetImpl* kernelRet, int ret, __code next(...)) {
    int num = proc->cbc_arg.cbc_console_arg.num;
    if (num != SYS_exec) {
        proc->tf->r0 = ret;
    }
    goto trapret();
}

extern __code exit(void);


__code exitKernelRetImpl(struct KernelRetImpl* kernelRet, __code next(...)) {
    goto exit();
}

extern __code swtch(void);

__code swtchKernelRetImpl(struct KernelRetImpl* kernelRet, __code next(...)) {
    goto swtch();
}

# システムコールエントリ

  • execだけもつInterface
    • 番号の対応とかは事前にメタ計算で解決する
1
2
3
4
typedef struct SyscallEntry <Type, Impl> {
  __code exec(Impl* syscall_entry, __code next(...));
  __code next(....);
} SyscallEntry;
  • イメージ的にはこんな感じ?
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
#include "../context.h"
#interface "SyscallEntry.h"

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

SyscallEntry* createReadSyscallEntry(struct Context* cbc_context) {
    struct SyscallEntry* syscall_entry  = new SyscallEntry();
    struct ReadSyscallEntry* read_syscall_entry = new ReadSyscallEntry();
    syscall_entry->syscall_entry = (union Data*)read_syscall_entry;
    syscall_entry->exec = C_execReadSyscallEntry;
    return syscall_entry;
}
__code execReadSyscallEntry(struct ReadSyscallEntry* syscall_entry, __code next(...)) {

    goto file_read(...);
}

# proc.cbc関連

  • プロセス操作で既に__ncodeになってる人々
1
2
3
4
5
6
7
8
9
typedef struct CbCProc <Type, Impl> {
  __code sched(Impl* cbc_proc, __code next(...));
  __code sleep(Impl* cbc_proc, struct spinlock* lk, __code next(...));
  __code sleep1(Impl* cbc_proc, __code next1(...));
  __code wakeup(Impl* cbc_proc, void* chan, __code next1(...));
  __code wakeup1(Impl* cbc_proc, void* chan, __code next(...));
  __code next(....);
  __code next1(...);
} CbCProc;
  • 実装を書いたので動かしてみる
    • 大域変数なプロセステーブル(ptable)をとりあえずヘッダファイルにしてproc.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
 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
#include "types.h"
#include "defs.h"
#include "param.h"
#include "memlayout.h"
#include "mmu.h"
#include "arm.h"
#include "proc.h"
#include "spinlock.h"
#include "ptable.h"

#include "kernel.h"

#interface "CbCProc.h"

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

CbCProc* createCbCProcImpl(struct Context* cbc_context) {
    struct CbCProc* cbc_proc  = new CbCProc();
    struct CbCProcImpl* cb_c_proc_impl = new CbCProcImpl();
    cbc_proc->cbc_proc = (union Data*)cb_c_proc_impl;
    cbc_proc->sched = C_schedCbCProcImpl;
    cbc_proc->sleep = C_sleepCbCProcImpl;
    cbc_proc->sleep1 = C_sleep1CbCProcImpl;
    cbc_proc->wakeup = C_wakeupCbCProcImpl;
    cbc_proc->wakeup1 = C_wakeup1CbCProcImpl;
    return cbc_proc;
}

__code schedCbCProcImpl(struct CbCProcImpl* cbc_proc, __code next(...)) {
    int intena;

    if(!holding(&ptable.lock)) {
        panic("sched ptable.lock");
    }

    if(cpu->ncli != 1) {
        panic("sched locks");
    }

    if(proc->state == RUNNING) {
        panic("sched running");
    }

    if(int_enabled ()) {
        panic("sched interruptible");
    }

    intena = cpu->intena;
    swtch(&proc->context, cpu->scheduler);
    cpu->intena = intena;

    goto next(...);
}

__code sleepCbCProcImpl(struct CbCProcImpl* cbc_proc, void* chan, struct spinlock* lk, __code next(...)) {
    //show_callstk("sleep");

    if(proc == 0) {
        panic("sleep");
    }

    if(lk == 0) {
        panic("sleep without lk");
    }

    if(lk != &ptable.lock){  //DOC: sleeplock0
        acquire(&ptable.lock);  //DOC: sleeplock1
        release(lk);
    }
    proc->chan = chan;
    proc->state = SLEEPING;
    proc->lk = lk;

    goto schedCbCProcImpl(cbc_sleep1);
}

__code sleepCbCProcImpl_stub(struct Context* cbc_context) {
     CbCProcImpl* cbc_proc = (CbCProcImpl*)GearImpl(cbc_context, CbCProc, cbc_proc);
     struct spinlock* lk = Gearef(cbc_context, CbCProc)->lk;
     void* chan = Gearef(cbc_context, CbCProc)->chan;
     enum Code next = Gearef(cbc_context, CbCProc)->next;
     goto sleepCbCProcImpl(cbc_context, cbc_proc, chan, lk, next);
}


__code sleep1CbCProcImpl(struct CbCProcImpl* cbc_proc, __code next1(...)) {
    struct spinlock *lk = proc->lk;
    // Tidy up.
    proc->chan = 0;

    // Reacquire original lock.
    if(lk != &ptable.lock){  //DOC: sleeplock2
        release(&ptable.lock);
        acquire(lk);
    }

    goto next1(...);
}

__code wakeupCbCProcImpl(struct CbCProcImpl* cbc_proc, void* chan, __code next1(...)) {
    acquire(&ptable.lock);
    goto wakeup1CbCProcImpl(chan);
}

__code wakeup1CbCProcImpl(struct CbCProcImpl* cbc_proc, void* chan, __code next(...)) {
    struct proc *p;

    for(p = ptable.proc; p < &ptable.proc[NPROC]; p++) {
        if(p->state == SLEEPING && p->chan == chan) {
            p->state = RUNNABLE;
        }
    }

    release(&ptable.lock);
    goto next(...);
}

# 現状

  • スタックフレームがおかしい
  • interfaceに無い構造体を引数で保つ場合はstubを手書きしないと型エラー
    • structがgenerate_stubでGearefの左辺から落とされる

# スタックフレームがおかしい

# 通常のsyscall (関数呼び出し->goto meta)

1
2
3
4
(gdb) bt
#0  cbc_returnKernelRetImpl_stub (cbc_context=0x87ffd000) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/impl/KernelRetImpl.c:37
#1  0x80033d3c in trap_swi () at /mnt/dalmore-home/one/src/cbcxv6/src/trap_asm.S:30
#2  0x00000000 in ?? ()

# read

1
2
3
4
5
6
7
(gdb) bt
#0  cbc_ret (ret=1) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/syscall.c:170
#1  0x80023764 in cbc_read (next=0x800231b4 <cbc_ret>) at /mnt/dalmore-home/one/build/cbcxv6/CMakeFiles/kernel.dir/c/sysfile.c:88
#2  0x80033d3c in trap_swi () at /mnt/dalmore-home/one/src/cbcxv6/src/trap_asm.S:30
#3  0x000019dc in ?? ()
Backtrace stopped: previous frame identical to this frame (corrupt stack?)
(gdb) up

readの場合は余計なスタックが乗っていて駄目

  • goto metaに統一させればtail callになりそうなので、readのInterface化を目指す

# 構造体の問題

  • この場合spinlockはtypedefしてないのでstructつけないといけないけど外される
    • 全部typedefすれば良いのだけど…
1
2
3
4
5
6
7
__code sleepCbCProcImpl_stub(struct Context* cbc_context) {
     CbCProcImpl* cbc_proc = (CbCProcImpl*)GearImpl(cbc_context, CbCProc, cbc_proc);
     struct spinlock* lk = Gearef(cbc_context, CbCProc)->lk;
     void* chan = Gearef(cbc_context, CbCProc)->chan;
     enum Code next = Gearef(cbc_context, CbCProc)->next;
     goto sleepCbCProcImpl(cbc_context, cbc_proc, chan, lk, next);
}
Licensed under CC BY-NC-SA 4.0
comments powered by Disqus
Built with Hugo
Theme Stack designed by Jimmy